diff options
| author | Pierre-Marie Pédrot | 2020-09-23 17:56:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-21 12:27:39 +0200 |
| commit | 9a3d4e284a03942e8a2b1f9d87a0b349702eaaa9 (patch) | |
| tree | 796075d0664347a8704fd53ca1a96a0d1a48abfd /kernel/constr.ml | |
| parent | 373376b734343d86aecc8d1f91a8c78eefa2b6cc (diff) | |
Add missing deprecations in Projection API.
Diffstat (limited to 'kernel/constr.ml')
| -rw-r--r-- | kernel/constr.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index d538ad7784..3157ec9f57 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -950,7 +950,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t let len = Array.length l1 in Int.equal len (Array.length l2) && leq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2 - | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq 0 c1 c2 + | Proj (p1,c1), Proj (p2,c2) -> Projection.CanOrd.equal p1 p2 && eq 0 c1 c2 | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && List.equal (eq 0) l1 l2 | Const (c1,u1), Const (c2,u2) -> (* The args length currently isn't used but may as well pass it. *) @@ -1158,7 +1158,7 @@ let constr_ord_int f t1 t2 = ((Int.compare =? (Array.compare f)) ==? (Array.compare f)) ln1 ln2 tl1 tl2 bl1 bl2 | CoFix _, _ -> -1 | _, CoFix _ -> 1 - | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2 + | Proj (p1,c1), Proj (p2,c2) -> (Projection.CanOrd.compare =? f) p1 p2 c1 c2 | Proj _, _ -> -1 | _, Proj _ -> 1 | Int i1, Int i2 -> Uint63.compare i1 i2 | Int _, _ -> -1 | _, Int _ -> 1 @@ -1456,7 +1456,7 @@ let rec hash t = | Meta n -> combinesmall 15 n | Rel n -> combinesmall 16 n | Proj (p,c) -> - combinesmall 17 (combine (Projection.hash p) (hash c)) + combinesmall 17 (combine (Projection.CanOrd.hash p) (hash c)) | Int i -> combinesmall 18 (Uint63.hash i) | Float f -> combinesmall 19 (Float64.hash f) | Array(u,t,def,ty) -> |