aboutsummaryrefslogtreecommitdiff
path: root/kernel/cooking.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-09-23 13:58:13 +0200
committerPierre-Marie Pédrot2020-10-21 12:23:19 +0200
commitaa3d78fefde6897a50273c83f944b6617963a9bc (patch)
treec24d9916af4b51762d4bde46f3ac5ea78d9c09d6 /kernel/cooking.ml
parentbc108fdf6cf42f3ce550f2f258adf7de5fa5bfdc (diff)
Similar introduction of a Construct module in the Names API.
Diffstat (limited to 'kernel/cooking.ml')
-rw-r--r--kernel/cooking.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index cb33bb729c..3707a75157 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -39,13 +39,13 @@ struct
let equal gr1 gr2 = match gr1, gr2 with
| ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2
| IndRef i1, IndRef i2 -> Ind.SyntacticOrd.equal i1 i2
- | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2
+ | ConstructRef c1, ConstructRef c2 -> Construct.SyntacticOrd.equal c1 c2
| _ -> false
open Hashset.Combine
let hash = function
| ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c)
| IndRef i -> combinesmall 2 (Ind.SyntacticOrd.hash i)
- | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c)
+ | ConstructRef c -> combinesmall 3 (Construct.SyntacticOrd.hash c)
end
module RefTable = Hashtbl.Make(RefHash)