fix hash_kind vs hcons

SkySkimmer · Jun 12, 2024 · 435e5eb · 435e5eb
1 parent f91f5c7
commit 435e5eb
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/kernel/hConstr.ml b/kernel/hConstr.ml
@@ -232,7 +232,7 @@ let rec hash_term (t : t) =
     (** FIXME: use a dedicated hashconsing structure *)
     let hcons_ctx (lna, c) =
       let () = Array.iteri (fun i x -> Array.unsafe_set lna i (hcons_annot x)) lna in
-      let fold accu na = combine (hash_annot na) accu in
+      let fold accu na = combine accu (hash_annot na) in
       let hna = Array.fold_left fold 0 lna in
       let c, hc = sh_rec c in
       (lna, c), combine hna hc
@@ -547,9 +547,9 @@ let hash_kind (type a) (hash:a -> int) = let open Hashset.Combine in function
     let h = combine5 (Instance.hash u) (hash c) hpms (hash_ctx p) hbl in
     combinesmall 12 h
   | Fix (_,(lna,tl,bl)) ->
-    combinesmall 13 (combine3 (hash_array hash_annot lna) (hash_array hash tl) (hash_array hash bl))
+    combinesmall 13 (combine3 (hash_array hash_annot lna) (hash_array hash bl) (hash_array hash tl))
   | CoFix (_,(lna,tl,bl)) ->
-    combinesmall 14 (combine3 (hash_array hash_annot lna) (hash_array hash tl) (hash_array hash bl))
+    combinesmall 14 (combine3 (hash_array hash_annot lna) (hash_array hash bl) (hash_array hash tl))
   | Meta _ -> assert false
   | Rel n -> combinesmall 16 n
   | Proj (p,_,c) -> combinesmall 17 (combine (Projection.SyntacticOrd.hash p) (hash c))