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 | |
| parent | 373376b734343d86aecc8d1f91a8c78eefa2b6cc (diff) | |
Add missing deprecations in Projection API.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.ml | 6 | ||||
| -rw-r--r-- | kernel/names.mli | 4 |
2 files changed, 7 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) -> diff --git a/kernel/names.mli b/kernel/names.mli index 2445d1f309..9a4ceef802 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -662,14 +662,18 @@ module Projection : sig val unfold : t -> t val equal : t -> t -> bool + [@@ocaml.deprecated "Use QProjection.equal"] val hash : t -> int + [@@ocaml.deprecated "Use QProjection.hash"] val hcons : t -> t (** Hashconsing of projections. *) val repr_equal : t -> t -> bool + [@@ocaml.deprecated "Use an explicit projection of Repr"] (** Ignoring the unfolding boolean. *) val compare : t -> t -> int + [@@ocaml.deprecated "Use QProjection.compare"] val map : (MutInd.t -> MutInd.t) -> t -> t val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t |