diff options
| author | Pierre-Marie Pédrot | 2020-09-23 13:58:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-21 12:23:19 +0200 |
| commit | aa3d78fefde6897a50273c83f944b6617963a9bc (patch) | |
| tree | c24d9916af4b51762d4bde46f3ac5ea78d9c09d6 /kernel/constr.ml | |
| parent | bc108fdf6cf42f3ce550f2f258adf7de5fa5bfdc (diff) | |
Similar introduction of a Construct module in the Names API.
Diffstat (limited to 'kernel/constr.ml')
| -rw-r--r-- | kernel/constr.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index b453a55d88..d538ad7784 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -355,7 +355,7 @@ let isRefX x c = match x, kind c with | ConstRef c, Const (c', _) -> Constant.CanOrd.equal c c' | IndRef i, Ind (i', _) -> Ind.CanOrd.equal i i' - | ConstructRef i, Construct (i', _) -> eq_constructor i i' + | ConstructRef i, Construct (i', _) -> Construct.CanOrd.equal i i' | VarRef id, Var id' -> Id.equal id id' | _ -> false @@ -957,7 +957,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t Constant.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstRef c1, nargs)) u1 u2 | Ind (c1,u1), Ind (c2,u2) -> Ind.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.IndRef c1, nargs)) u1 u2 | Construct (c1,u1), Construct (c2,u2) -> - eq_constructor c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2 + Construct.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2 | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) -> eq 0 p1 p2 && eq_invert (eq 0) (leq_universes None) iv1 iv2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2 | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> @@ -1141,7 +1141,7 @@ let constr_ord_int f t1 t2 = | Const _, _ -> -1 | _, Const _ -> 1 | Ind (ind1, _u1), Ind (ind2, _u2) -> Ind.CanOrd.compare ind1 ind2 | Ind _, _ -> -1 | _, Ind _ -> 1 - | Construct (ct1,_u1), Construct (ct2,_u2) -> constructor_ord ct1 ct2 + | Construct (ct1,_u1), Construct (ct2,_u2) -> Construct.CanOrd.compare ct1 ct2 | Construct _, _ -> -1 | _, Construct _ -> 1 | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) -> let c = f p1 p2 in @@ -1335,7 +1335,7 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = | Construct (c,u) -> let u', hu = sh_instance u in (Construct (sh_construct c, u'), - combinesmall 11 (combine (constructor_syntactic_hash c) hu)) + combinesmall 11 (combine (Construct.SyntacticOrd.hash c) hu)) | Case (ci,p,iv,c,bl) -> let p, hp = sh_rec p and iv, hiv = sh_invert iv @@ -1446,7 +1446,7 @@ let rec hash t = | Ind (ind,u) -> combinesmall 10 (combine (Ind.CanOrd.hash ind) (Instance.hash u)) | Construct (c,u) -> - combinesmall 11 (combine (constructor_hash c) (Instance.hash u)) + combinesmall 11 (combine (Construct.CanOrd.hash c) (Instance.hash u)) | Case (_ , p, iv, c, bl) -> combinesmall 12 (combine4 (hash c) (hash p) (hash_invert iv) (hash_term_array bl)) | Fix (_ln ,(_, tl, bl)) -> |