Correct handling of hashconsing of constraint sets. The previous implementation

did not respect the requirement that equality should preserve hash.

1 files changed, 20 insertions, 24 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index fa0c431e3..551d74043 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -637,17 +637,19 @@ let enforce_constraint cst g =
     | (u,Le,v) -> enforce_univ_leq u v g
     | (u,Eq,v) -> enforce_univ_eq u v g
 
-module Constraint = Set.Make(
-  struct
-    type t = univ_constraint
-    let compare (u,c,v) (u',c',v') =
-      let i = constraint_type_ord c c' in
-      if not (Int.equal i 0) then i
-      else
-	let i' = UniverseLevel.compare u u' in
-	if not (Int.equal i' 0) then i'
-	else UniverseLevel.compare v v'
-  end)
+module UConstraintOrd =
+struct
+  type t = univ_constraint
+  let compare (u,c,v) (u',c',v') =
+    let i = constraint_type_ord c c' in
+    if not (Int.equal i 0) then i
+    else
+      let i' = UniverseLevel.compare u u' in
+      if not (Int.equal i' 0) then i'
+      else UniverseLevel.compare v v'
+end
+
+module Constraint = Set.Make(UConstraintOrd)
 
 type constraints = Constraint.t
 
@@ -1075,19 +1077,13 @@ module Hconstraint =
       let hash = Hashtbl.hash
     end)
 
-module Hconstraints =
-  Hashcons.Make(
-    struct
-      type t = constraints
-      type u = univ_constraint -> univ_constraint
-      let hashcons huc s =
-	Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty
-      let equal s s' =
-	List.for_all2eq (==)
-	  (Constraint.elements s)
-	  (Constraint.elements s')
-      let hash = Hashtbl.hash
-    end)
+module UConstraintHash =
+struct
+  type t = univ_constraint
+  let hash = Hashtbl.hash
+end
+
+module Hconstraints = Set.Hashcons(UConstraintOrd)(UConstraintHash)
 
 let hcons_constraint = Hashcons.simple_hcons Hconstraint.generate hcons_univlevel
 let hcons_constraints = Hashcons.simple_hcons Hconstraints.generate hcons_constraint