diff options
| -rw-r--r-- | kernel/constr.ml | 6 | ||||
| -rw-r--r-- | kernel/names.mli | 4 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 2 | ||||
| -rw-r--r-- | pretyping/constr_matching.ml | 4 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 2 | ||||
| -rw-r--r-- | tactics/cbn.ml | 2 |
7 files changed, 13 insertions, 9 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 diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 38b26d06b9..a7ebd5f9f5 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -240,7 +240,7 @@ let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with let same_proj sigma t1 t2 = match EConstr.kind sigma t1, EConstr.kind sigma t2 with - | Proj(c1,_), Proj(c2, _) -> Projection.equal c1 c2 + | Proj(c1,_), Proj(c2, _) -> Projection.CanOrd.equal c1 c2 | _ -> false let all_ok _ _ = true diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index d394bd1288..a3f1c0b004 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -311,7 +311,7 @@ let matches_core env sigma allow_bound_rels || Projection.unfolded pr -> raise PatternMatchingFailure | PProj (pr1,c1), Proj (pr,c) -> - if Projection.equal pr1 pr then + if Environ.QProjection.equal env pr1 pr then try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c) arg1 arg2 with Invalid_argument _ -> raise PatternMatchingFailure else raise PatternMatchingFailure @@ -332,7 +332,7 @@ let matches_core env sigma allow_bound_rels sorec ctx env subst p term with Retyping.RetypeError _ -> raise PatternMatchingFailure) - | PProj (p1,c1), Proj (p2,c2) when Projection.equal p1 p2 -> + | PProj (p1,c1), Proj (p2,c2) when Environ.QProjection.equal env p1 p2 -> sorec ctx env subst c1 c2 | PProd (na1,c1,d1), Prod(na2,c2,d2) -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 1940668519..90af143a2d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -831,7 +831,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty in ise_try evd [f1; f2] - | Proj (p, c), Proj (p', c') when Projection.repr_equal p p' -> + | Proj (p, c), Proj (p', c') when QProjection.Repr.equal env (Projection.repr p) (Projection.repr p') -> let f1 i = ise_and i [(fun i -> evar_conv_x flags env i CONV c c'); diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index b5c83b75f9..b259945d9e 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -59,7 +59,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with | PCoFix (i1,f1), PCoFix (i2,f2) -> Int.equal i1 i2 && rec_declaration_eq f1 f2 | PProj (p1, t1), PProj (p2, t2) -> - Projection.equal p1 p2 && constr_pattern_eq t1 t2 + Projection.CanOrd.equal p1 p2 && constr_pattern_eq t1 t2 | PInt i1, PInt i2 -> Uint63.equal i1 i2 | PFloat f1, PFloat f2 -> diff --git a/tactics/cbn.ml b/tactics/cbn.ml index 5838bbcc19..31873ea6b0 100644 --- a/tactics/cbn.ml +++ b/tactics/cbn.ml @@ -226,7 +226,7 @@ struct match x, y with | Cst_const (c1,u1), Cst_const (c2, u2) -> Constant.CanOrd.equal c1 c2 && Univ.Instance.equal u1 u2 - | Cst_proj p1, Cst_proj p2 -> Projection.repr_equal p1 p2 + | Cst_proj p1, Cst_proj p2 -> Projection.Repr.CanOrd.equal (Projection.repr p1) (Projection.repr p2) | _, _ -> false in let rec equal_rec sk1 sk2 = |