From 9f81b58551958aea2a85bcdd0cc3f88bf4634c92 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 29 Jul 2015 01:26:00 +0200
Subject: Fixing bug #4289 (hash-consing only user part of constant not
 compatible with a unique bound module name counter which is not synchronous
 with the backtracking).

We changed hash-consing of kernel name pairs to a purely memory
management issue, not trying to exploit logical properties such as
"syntactically equal user names have syntactically same canonical
names" (which is true in a given logical session, but not in memory,
at least because of residual values after backtracking).
---
 kernel/names.ml | 24 +++++++++++++++++-------
 1 file changed, 17 insertions(+), 7 deletions(-)

(limited to 'kernel/names.ml')

diff --git a/kernel/names.ml b/kernel/names.ml
index f217c932cc..19fe62ec85 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -453,6 +453,9 @@ module KNset = KNmap.Set
     - when user and canonical parts differ, we cannot be in a section
       anymore, hence the dirpath must be empty
     - two pairs with the same user part should have the same canonical part
+      in a given environment (though with backtracking, the hash-table can
+      contains pairs with same user part but different canonical part from
+      a previous state of the session)
 
    Note: since most of the time the canonical and user parts are equal,
    we handle this case with a particular constructor to spare some memory *)
@@ -504,7 +507,7 @@ module KerPair = struct
   let debug_print kp = str (debug_to_string kp)
 
   (** For ordering kernel pairs, both user or canonical parts may make
-      sense, according to your needs : user for the environments, canonical
+      sense, according to your needs: user for the environments, canonical
       for other uses (ex: non-logical things). *)
 
   module UserOrd = struct
@@ -521,16 +524,18 @@ module KerPair = struct
     let hash x = KerName.hash (canonical x)
   end
 
-  (** Default comparison is on the canonical part *)
+  (** Default (logical) comparison is on the canonical part *)
   let equal = CanOrd.equal
 
-  (** Hash-consing : we discriminate only on the user part, since having
-      the same user part implies having the same canonical part
-      (invariant of the system). *)
+  (** Hash-consing (despite having the same user part implies having
+      the same canonical part is a logical invariant of the system, it
+      is not necessarily an invariant in memory, so we treat kernel
+      names as they are syntactically for hash-consing) *)
 
   let hash = function
   | Same kn -> KerName.hash kn
-  | Dual (kn, _) -> KerName.hash kn
+  | Dual (knu, knc) ->
+    Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc)
 
   module Self_Hashcons =
     struct
@@ -539,7 +544,12 @@ module KerPair = struct
       let hashcons hkn = function
         | Same kn -> Same (hkn kn)
         | Dual (knu,knc) -> make (hkn knu) (hkn knc)
-      let equal x y = (user x) == (user y)
+      let equal x y = (* physical comparison on subterms *)
+        x == y ||
+        match x,y with
+        | Same x, Same y -> x == y
+        | Dual (ux,cx), Dual (uy,cy) -> ux == uy && cx == cy
+        | (Same _ | Dual _), _ -> false
       let hash = hash
     end
 
-- 
cgit v1.2.3


From 1ee23d71dadd6211c36afe8d2891b7170535cd62 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Jul 2015 15:55:24 +0200
Subject: Followup of 9f81b58551.

The hash function exported by the interface ought to respect the equality.
Therefore, we only use the syntactic hash for the hashconsing module while
using the canonical hash in the API.
---
 kernel/names.ml | 22 ++++++++++------------
 1 file changed, 10 insertions(+), 12 deletions(-)

(limited to 'kernel/names.ml')

diff --git a/kernel/names.ml b/kernel/names.ml
index 19fe62ec85..ae2b3b6389 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -524,18 +524,9 @@ module KerPair = struct
     let hash x = KerName.hash (canonical x)
   end
 
-  (** Default (logical) comparison is on the canonical part *)
+  (** Default (logical) comparison and hash is on the canonical part *)
   let equal = CanOrd.equal
-
-  (** Hash-consing (despite having the same user part implies having
-      the same canonical part is a logical invariant of the system, it
-      is not necessarily an invariant in memory, so we treat kernel
-      names as they are syntactically for hash-consing) *)
-
-  let hash = function
-  | Same kn -> KerName.hash kn
-  | Dual (knu, knc) ->
-    Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc)
+  let hash = CanOrd.hash
 
   module Self_Hashcons =
     struct
@@ -550,7 +541,14 @@ module KerPair = struct
         | Same x, Same y -> x == y
         | Dual (ux,cx), Dual (uy,cy) -> ux == uy && cx == cy
         | (Same _ | Dual _), _ -> false
-      let hash = hash
+      (** Hash-consing (despite having the same user part implies having
+          the same canonical part is a logical invariant of the system, it
+          is not necessarily an invariant in memory, so we treat kernel
+          names as they are syntactically for hash-consing) *)
+      let hash = function
+      | Same kn -> KerName.hash kn
+      | Dual (knu, knc) ->
+        Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc)
     end
 
   module HashKP = Hashcons.Make(Self_Hashcons)
-- 
cgit v1.2.3


From f556da10a117396c2c796f6915321b67849f65cd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 31 Jul 2015 18:53:21 +0200
Subject: Adding eq/compare/hash for syntactic view at
 constant/inductive/constructor kernel_name pairs rather than viewing them
 from only the user or canonical part.

Hopefully more uniformity in Constr.hasheq (using systematically == on
subterms).

A semantic change: Cooking now indexing again on full pairs of kernel
names rather than only on the canonical names, so as to preserve user
name.

Also, in pair of kernel names, ensuring the compact representation is
used as soon as both names are the same.
---
 kernel/names.ml | 42 +++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 41 insertions(+), 1 deletion(-)

(limited to 'kernel/names.ml')

diff --git a/kernel/names.ml b/kernel/names.ml
index ae2b3b6389..bc33932086 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -477,7 +477,7 @@ module KerPair = struct
     | Dual (kn,_) -> kn
 
   let same kn = Same kn
-  let make knu knc = if knu == knc then Same knc else Dual (knu,knc)
+  let make knu knc = if KerName.equal knu knc then Same knc else Dual (knu,knc)
 
   let make1 = same
   let make2 mp l = same (KerName.make2 mp l)
@@ -524,6 +524,23 @@ module KerPair = struct
     let hash x = KerName.hash (canonical x)
   end
 
+  module SyntacticOrd = struct
+    type t = kernel_pair
+    let compare x y = match x, y with
+      | Same knx, Same kny -> KerName.compare knx kny
+      | Dual (knux,kncx), Dual (knuy,kncy) ->
+        let c = KerName.compare knux knuy in
+        if not (Int.equal c 0) then c
+        else KerName.compare kncx kncy
+      | Same _, _ -> -1
+      | Dual _, _ -> 1
+    let equal x y = x == y || compare x y = 0
+    let hash = function
+      | Same kn -> KerName.hash kn
+      | Dual (knu, knc) ->
+        Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc)
+  end
+
   (** Default (logical) comparison and hash is on the canonical part *)
   let equal = CanOrd.equal
   let hash = CanOrd.hash
@@ -590,6 +607,8 @@ let index_of_constructor (ind, i) = i
 let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2
 let eq_user_ind (m1, i1) (m2, i2) =
   Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2
+let eq_syntactic_ind (m1, i1) (m2, i2) =
+  Int.equal i1 i2 && MutInd.SyntacticOrd.equal m1 m2
 
 let ind_ord (m1, i1) (m2, i2) =
   let c = Int.compare i1 i2 in
@@ -597,15 +616,22 @@ let ind_ord (m1, i1) (m2, i2) =
 let ind_user_ord (m1, i1) (m2, i2) =
   let c = Int.compare i1 i2 in
   if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c
+let ind_syntactic_ord (m1, i1) (m2, i2) =
+  let c = Int.compare i1 i2 in
+  if Int.equal c 0 then MutInd.SyntacticOrd.compare m1 m2 else c
 
 let ind_hash (m, i) =
   Hashset.Combine.combine (MutInd.hash m) (Int.hash i)
 let ind_user_hash (m, i) =
   Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i)
+let ind_syntactic_hash (m, i) =
+  Hashset.Combine.combine (MutInd.SyntacticOrd.hash m) (Int.hash i)
 
 let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2
 let eq_user_constructor (ind1, j1) (ind2, j2) =
   Int.equal j1 j2 && eq_user_ind ind1 ind2
+let eq_syntactic_constructor (ind1, j1) (ind2, j2) =
+  Int.equal j1 j2 && eq_syntactic_ind ind1 ind2
 
 let constructor_ord (ind1, j1) (ind2, j2) =
   let c = Int.compare j1 j2 in
@@ -613,11 +639,16 @@ let constructor_ord (ind1, j1) (ind2, j2) =
 let constructor_user_ord (ind1, j1) (ind2, j2) =
   let c = Int.compare j1 j2 in
   if Int.equal c 0 then ind_user_ord ind1 ind2 else c
+let constructor_syntactic_ord (ind1, j1) (ind2, j2) =
+  let c = Int.compare j1 j2 in
+  if Int.equal c 0 then ind_syntactic_ord ind1 ind2 else c
 
 let constructor_hash (ind, i) =
   Hashset.Combine.combine (ind_hash ind) (Int.hash i)
 let constructor_user_hash (ind, i) =
   Hashset.Combine.combine (ind_user_hash ind) (Int.hash i)
+let constructor_syntactic_hash (ind, i) =
+  Hashset.Combine.combine (ind_syntactic_hash ind) (Int.hash i)
 
 module InductiveOrdered = struct
   type t = inductive
@@ -805,6 +836,15 @@ struct
 
   let hash (c, b) = (if b then 0 else 1) + Constant.hash c
 
+  module SyntacticOrd = struct
+    type t = constant * bool
+    let compare (c, b) (c', b') =
+      if b = b' then Constant.SyntacticOrd.compare c c' else -1
+    let equal (c, b as x) (c', b' as x') =
+      x == x' || b = b' && Constant.SyntacticOrd.equal c c'
+    let hash (c, b) = (if b then 0 else 1) + Constant.SyntacticOrd.hash c
+  end
+
   module Self_Hashcons =
     struct
       type _t = t
-- 
cgit v1.2.3


From 979de570714d340aaab7a6e99e08d46aa616e7da Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Aug 2015 14:45:24 +0200
Subject: A patch renaming equal into eq in the module dealing with
 hash-consing, so as to avoid having too many kinds of equalities with same
 name.

---
 kernel/names.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'kernel/names.ml')

diff --git a/kernel/names.ml b/kernel/names.ml
index bc33932086..a99702d159 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -102,7 +102,7 @@ struct
       let hashcons hident = function
         | Name id -> Name (hident id)
         | n -> n
-      let equal n1 n2 =
+      let eq n1 n2 =
         n1 == n2 ||
         match (n1,n2) with
           | (Name id1, Name id2) -> id1 == id2
@@ -236,7 +236,7 @@ struct
       type t = _t
       type u = (Id.t -> Id.t) * (DirPath.t -> DirPath.t)
       let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
-      let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
+      let eq ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
         (x == y) ||
         (Int.equal n1 n2 && s1 == s2 && dir1 == dir2)
       let hash = hash
@@ -327,7 +327,7 @@ module ModPath = struct
       | MPfile dir -> MPfile (hdir dir)
       | MPbound m -> MPbound (huniqid m)
       | MPdot (md,l) -> MPdot (hashcons hfuns md, hstr l)
-    let rec equal d1 d2 =
+    let rec eq d1 d2 =
       d1 == d2 ||
       match d1,d2 with
       | MPfile dir1, MPfile dir2 -> dir1 == dir2
@@ -423,7 +423,7 @@ module KerName = struct
     let hashcons (hmod,hdir,hstr) kn =
       let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in
       { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; }
-    let equal kn1 kn2 =
+    let eq kn1 kn2 =
       kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath &&
         kn1.knlabel == kn2.knlabel
     let hash = hash
@@ -552,7 +552,7 @@ module KerPair = struct
       let hashcons hkn = function
         | Same kn -> Same (hkn kn)
         | Dual (knu,knc) -> make (hkn knu) (hkn knc)
-      let equal x y = (* physical comparison on subterms *)
+      let eq x y = (* physical comparison on subterms *)
         x == y ||
         match x,y with
         | Same x, Same y -> x == y
@@ -693,7 +693,7 @@ module Hind = Hashcons.Make(
     type t = inductive
     type u = MutInd.t -> MutInd.t
     let hashcons hmind (mind, i) = (hmind mind, i)
-    let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2
+    let eq (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2
     let hash = ind_hash
   end)
 
@@ -702,7 +702,7 @@ module Hconstruct = Hashcons.Make(
     type t = constructor
     type u = inductive -> inductive
     let hashcons hind (ind, j) = (hind ind, j)
-    let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2
+    let eq (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2
     let hash = constructor_hash
   end)
 
@@ -851,7 +851,7 @@ struct
       type t = _t
       type u = Constant.t -> Constant.t
       let hashcons hc (c,b) = (hc c,b)
-      let equal ((c,b) as x) ((c',b') as y) =
+      let eq ((c,b) as x) ((c',b') as y) =
         x == y || (c == c' && b == b')
       let hash = hash
     end
-- 
cgit v1.2.3


From 35ba593b4ecb805b4e69c01c56fb4b93dfafdf0b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Aug 2015 19:31:00 +0200
Subject: Reverting 16 last commits, committed mistakenly using the wrong push
 command. Sorry so much.

Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
---
 kernel/names.ml | 58 +++++++++------------------------------------------------
 1 file changed, 9 insertions(+), 49 deletions(-)

(limited to 'kernel/names.ml')

diff --git a/kernel/names.ml b/kernel/names.ml
index a99702d159..ae2b3b6389 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -102,7 +102,7 @@ struct
       let hashcons hident = function
         | Name id -> Name (hident id)
         | n -> n
-      let eq n1 n2 =
+      let equal n1 n2 =
         n1 == n2 ||
         match (n1,n2) with
           | (Name id1, Name id2) -> id1 == id2
@@ -236,7 +236,7 @@ struct
       type t = _t
       type u = (Id.t -> Id.t) * (DirPath.t -> DirPath.t)
       let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
-      let eq ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
+      let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
         (x == y) ||
         (Int.equal n1 n2 && s1 == s2 && dir1 == dir2)
       let hash = hash
@@ -327,7 +327,7 @@ module ModPath = struct
       | MPfile dir -> MPfile (hdir dir)
       | MPbound m -> MPbound (huniqid m)
       | MPdot (md,l) -> MPdot (hashcons hfuns md, hstr l)
-    let rec eq d1 d2 =
+    let rec equal d1 d2 =
       d1 == d2 ||
       match d1,d2 with
       | MPfile dir1, MPfile dir2 -> dir1 == dir2
@@ -423,7 +423,7 @@ module KerName = struct
     let hashcons (hmod,hdir,hstr) kn =
       let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in
       { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; }
-    let eq kn1 kn2 =
+    let equal kn1 kn2 =
       kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath &&
         kn1.knlabel == kn2.knlabel
     let hash = hash
@@ -477,7 +477,7 @@ module KerPair = struct
     | Dual (kn,_) -> kn
 
   let same kn = Same kn
-  let make knu knc = if KerName.equal knu knc then Same knc else Dual (knu,knc)
+  let make knu knc = if knu == knc then Same knc else Dual (knu,knc)
 
   let make1 = same
   let make2 mp l = same (KerName.make2 mp l)
@@ -524,23 +524,6 @@ module KerPair = struct
     let hash x = KerName.hash (canonical x)
   end
 
-  module SyntacticOrd = struct
-    type t = kernel_pair
-    let compare x y = match x, y with
-      | Same knx, Same kny -> KerName.compare knx kny
-      | Dual (knux,kncx), Dual (knuy,kncy) ->
-        let c = KerName.compare knux knuy in
-        if not (Int.equal c 0) then c
-        else KerName.compare kncx kncy
-      | Same _, _ -> -1
-      | Dual _, _ -> 1
-    let equal x y = x == y || compare x y = 0
-    let hash = function
-      | Same kn -> KerName.hash kn
-      | Dual (knu, knc) ->
-        Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc)
-  end
-
   (** Default (logical) comparison and hash is on the canonical part *)
   let equal = CanOrd.equal
   let hash = CanOrd.hash
@@ -552,7 +535,7 @@ module KerPair = struct
       let hashcons hkn = function
         | Same kn -> Same (hkn kn)
         | Dual (knu,knc) -> make (hkn knu) (hkn knc)
-      let eq x y = (* physical comparison on subterms *)
+      let equal x y = (* physical comparison on subterms *)
         x == y ||
         match x,y with
         | Same x, Same y -> x == y
@@ -607,8 +590,6 @@ let index_of_constructor (ind, i) = i
 let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2
 let eq_user_ind (m1, i1) (m2, i2) =
   Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2
-let eq_syntactic_ind (m1, i1) (m2, i2) =
-  Int.equal i1 i2 && MutInd.SyntacticOrd.equal m1 m2
 
 let ind_ord (m1, i1) (m2, i2) =
   let c = Int.compare i1 i2 in
@@ -616,22 +597,15 @@ let ind_ord (m1, i1) (m2, i2) =
 let ind_user_ord (m1, i1) (m2, i2) =
   let c = Int.compare i1 i2 in
   if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c
-let ind_syntactic_ord (m1, i1) (m2, i2) =
-  let c = Int.compare i1 i2 in
-  if Int.equal c 0 then MutInd.SyntacticOrd.compare m1 m2 else c
 
 let ind_hash (m, i) =
   Hashset.Combine.combine (MutInd.hash m) (Int.hash i)
 let ind_user_hash (m, i) =
   Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i)
-let ind_syntactic_hash (m, i) =
-  Hashset.Combine.combine (MutInd.SyntacticOrd.hash m) (Int.hash i)
 
 let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2
 let eq_user_constructor (ind1, j1) (ind2, j2) =
   Int.equal j1 j2 && eq_user_ind ind1 ind2
-let eq_syntactic_constructor (ind1, j1) (ind2, j2) =
-  Int.equal j1 j2 && eq_syntactic_ind ind1 ind2
 
 let constructor_ord (ind1, j1) (ind2, j2) =
   let c = Int.compare j1 j2 in
@@ -639,16 +613,11 @@ let constructor_ord (ind1, j1) (ind2, j2) =
 let constructor_user_ord (ind1, j1) (ind2, j2) =
   let c = Int.compare j1 j2 in
   if Int.equal c 0 then ind_user_ord ind1 ind2 else c
-let constructor_syntactic_ord (ind1, j1) (ind2, j2) =
-  let c = Int.compare j1 j2 in
-  if Int.equal c 0 then ind_syntactic_ord ind1 ind2 else c
 
 let constructor_hash (ind, i) =
   Hashset.Combine.combine (ind_hash ind) (Int.hash i)
 let constructor_user_hash (ind, i) =
   Hashset.Combine.combine (ind_user_hash ind) (Int.hash i)
-let constructor_syntactic_hash (ind, i) =
-  Hashset.Combine.combine (ind_syntactic_hash ind) (Int.hash i)
 
 module InductiveOrdered = struct
   type t = inductive
@@ -693,7 +662,7 @@ module Hind = Hashcons.Make(
     type t = inductive
     type u = MutInd.t -> MutInd.t
     let hashcons hmind (mind, i) = (hmind mind, i)
-    let eq (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2
+    let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2
     let hash = ind_hash
   end)
 
@@ -702,7 +671,7 @@ module Hconstruct = Hashcons.Make(
     type t = constructor
     type u = inductive -> inductive
     let hashcons hind (ind, j) = (hind ind, j)
-    let eq (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2
+    let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2
     let hash = constructor_hash
   end)
 
@@ -836,22 +805,13 @@ struct
 
   let hash (c, b) = (if b then 0 else 1) + Constant.hash c
 
-  module SyntacticOrd = struct
-    type t = constant * bool
-    let compare (c, b) (c', b') =
-      if b = b' then Constant.SyntacticOrd.compare c c' else -1
-    let equal (c, b as x) (c', b' as x') =
-      x == x' || b = b' && Constant.SyntacticOrd.equal c c'
-    let hash (c, b) = (if b then 0 else 1) + Constant.SyntacticOrd.hash c
-  end
-
   module Self_Hashcons =
     struct
       type _t = t
       type t = _t
       type u = Constant.t -> Constant.t
       let hashcons hc (c,b) = (hc c,b)
-      let eq ((c,b) as x) ((c',b') as y) =
+      let equal ((c,b) as x) ((c',b') as y) =
         x == y || (c == c' && b == b')
       let hash = hash
     end
-- 
cgit v1.2.3