aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/evarconv.ml8
-rw-r--r--pretyping/evarsolve.ml12
-rw-r--r--pretyping/evd.ml36
-rw-r--r--pretyping/evd.mli8
-rw-r--r--pretyping/patternops.ml4
-rw-r--r--pretyping/unification.ml10
6 files changed, 46 insertions, 32 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0fd508604b..c436fed2c9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -830,7 +830,7 @@ let first_order_unification ts env evd (ev1,l1) (term2,l2) =
let choose_less_dependent_instance evk evd term args =
let evi = Evd.find_undefined evd evk in
let subst = make_pure_subst evi args in
- let subst' = List.filter (fun (id,c) -> eq_constr c term) subst in
+ let subst' = List.filter (fun (id,c) -> eq_constr evd c term) subst in
match subst' with
| [] -> None
| (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd)
@@ -840,7 +840,7 @@ let apply_on_subterm evdref f c t =
(* By using eq_constr, we make an approximation, for instance, we *)
(* could also be interested in finding a term u convertible to t *)
(* such that c occurs in u *)
- if eq_constr c t then f k
+ if eq_constr !evdref c t then f k
else
match kind_of_term t with
| Evar (evk,args) when Evd.is_undefined !evdref evk ->
@@ -1002,7 +1002,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
let app_empty = Array.is_empty l1 && Array.is_empty l2 in
match kind_of_term term1, kind_of_term term2 with
| Evar (evk1,args1), (Rel _|Var _) when app_empty
- && List.for_all (fun a -> eq_constr a term2 || isEvar a)
+ && List.for_all (fun a -> eq_constr evd a term2 || isEvar a)
(remove_instance_local_defs evd evk1 args1) ->
(* The typical kind of constraint coming from pattern-matching return
type inference *)
@@ -1010,7 +1010,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
| Some evd -> Success evd
| None -> UnifFailure (evd, ConversionFailed (env,term1,term2)))
| (Rel _|Var _), Evar (evk2,args2) when app_empty
- && List.for_all (fun a -> eq_constr a term1 || isEvar a)
+ && List.for_all (fun a -> eq_constr evd a term1 || isEvar a)
(remove_instance_local_defs evd evk2 args2) ->
(* The typical kind of constraint coming from pattern-matching return
type inference *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f32238ee72..4bffe3d1f7 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -351,7 +351,7 @@ let rec expand_and_check_vars aliases = function
module Constrhash = Hashtbl.Make
(struct type t = constr
- let equal = eq_constr
+ let equal = Term.eq_constr
let hash = hash_constr
end)
@@ -495,7 +495,7 @@ let make_projectable_subst aliases sigma evi args =
| Var id' ->
let idc = normalize_alias_var evar_aliases id' in
let sub = try Id.Map.find idc all with Not_found -> [] in
- if List.exists (fun (c,_,_) -> eq_constr a c) sub then
+ if List.exists (fun (c,_,_) -> eq_constr sigma a c) sub then
(rest,all,cstrs)
else
(rest,
@@ -648,15 +648,15 @@ let rec assoc_up_to_alias sigma aliases y yc = function
| [] -> raise Not_found
| (c,cc,id)::l ->
let c' = whd_evar sigma c in
- if eq_constr y c' then id
+ if eq_constr sigma y c' then id
else
match l with
| _ :: _ -> assoc_up_to_alias sigma aliases y yc l
| [] ->
(* Last chance, we reason up to alias conversion *)
match (if c == c' then cc else normalize_alias_opt aliases c') with
- | Some cc when eq_constr yc cc -> id
- | _ -> if eq_constr yc c then id else raise Not_found
+ | Some cc when eq_constr sigma yc cc -> id
+ | _ -> if eq_constr sigma yc c then id else raise Not_found
let rec find_projectable_vars with_evars aliases sigma y subst =
let yc = normalize_alias aliases y in
@@ -1172,7 +1172,7 @@ type conv_fun_bool =
* depend on these args). *)
let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 =
- if Array.equal eq_constr argsv1 argsv2 then evd else
+ if Array.equal (eq_constr evd) argsv1 argsv2 then evd else
(* Filter and restrict if needed *)
let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in
let untypedfilter =
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index aa2ca0009b..bd105c7287 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -198,19 +198,6 @@ let evar_filtered_env evi = match Filter.repr (evar_filter evi) with
in
make_env filter (evar_context evi)
-let eq_evar_body b1 b2 = match b1, b2 with
-| Evar_empty, Evar_empty -> true
-| Evar_defined t1, Evar_defined t2 -> eq_constr t1 t2
-| _ -> false
-
-let eq_evar_info ei1 ei2 =
- ei1 == ei2 ||
- eq_constr ei1.evar_concl ei2.evar_concl &&
- eq_named_context_val (ei1.evar_hyps) (ei2.evar_hyps) &&
- eq_evar_body ei1.evar_body ei2.evar_body
- (** ppedrot: [eq_constr] may be a bit too permissive here *)
-
-
let map_evar_body f = function
| Evar_empty -> Evar_empty
| Evar_defined d -> Evar_defined (f d)
@@ -1346,6 +1333,29 @@ let test_conversion env d pb t u =
try conversion_gen env d pb t u; true
with _ -> false
+let eq_constr d t u =
+ Term.eq_constr_univs d.universes.uctx_universes t u
+
+let eq_named_context_val d ctx1 ctx2 =
+ ctx1 == ctx2 ||
+ let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
+ let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
+ Id.equal i1 i2 && Option.equal (eq_constr d) c1 c2 && (eq_constr d) t1 t2
+ in List.equal eq_named_declaration c1 c2
+
+let eq_evar_body d b1 b2 = match b1, b2 with
+| Evar_empty, Evar_empty -> true
+| Evar_defined t1, Evar_defined t2 -> eq_constr d t1 t2
+| _ -> false
+
+let eq_evar_info d ei1 ei2 =
+ ei1 == ei2 ||
+ eq_constr d ei1.evar_concl ei2.evar_concl &&
+ eq_named_context_val d (ei1.evar_hyps) (ei2.evar_hyps) &&
+ eq_evar_body d ei1.evar_body ei2.evar_body
+ (** ppedrot: [eq_constr] may be a bit too permissive here *)
+
+
(**********************************************************)
(* Accessing metas *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index bbae32d8ca..d0a47fe96e 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -103,8 +103,6 @@ type evar_info = {
(** Extra store, used for clever hacks. *)
}
-val eq_evar_info : evar_info -> evar_info -> bool
-
val make_evar : named_context_val -> types -> evar_info
val evar_concl : evar_info -> constr
val evar_context : evar_info -> named_context
@@ -214,6 +212,9 @@ val add_constraints : evar_map -> Univ.constraints -> evar_map
val undefined_map : evar_map -> evar_info Evar.Map.t
(** Access the undefined evar mapping directly. *)
+val eq_evar_info : evar_map -> evar_info -> evar_info -> bool
+(** Compare the evar_info's up to the universe constraints of the evar map. *)
+
(** {6 Instantiating partial terms} *)
exception NotInstantiatedEvar
@@ -517,6 +518,9 @@ val conversion : env -> evar_map -> conv_pb -> constr -> constr -> evar_map
(** This one forgets about the assignemts of universes. *)
val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool
+(** Syntactic equality up to universe constraints. *)
+val eq_constr : evar_map -> constr -> constr -> bool
+
(********************************************************************
constr with holes *)
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 54ce29bf71..44ff2b5b8c 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -75,8 +75,8 @@ and cofixpoint_eq (i1, r1) (i2, r2) =
and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) =
Array.equal Name.equal n1 n2 &&
- Array.equal eq_constr c1 c2 &&
- Array.equal eq_constr r1 r2
+ Array.equal Term.eq_constr c1 c2 &&
+ Array.equal Term.eq_constr r1 r2
let rec occur_meta_pattern = function
| PApp (f,args) ->
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 937d84972b..7530ced7c0 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -389,7 +389,7 @@ let expand_key ts env sigma = function
| Some (IsProj (p, c)) ->
let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma
Cst_stack.empty (c, unfold_projection env p [])))
- in if eq_constr (mkProj (p, c)) red then None else Some red
+ in if Term.eq_constr (mkProj (p, c)) red then None else Some red
| None -> None
let subterm_restriction is_subterm flags =
@@ -717,11 +717,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
and reduce curenvnb pb b wt (sigma, metas, evars as substn) cM cN =
if use_full_betaiota flags && not (subterm_restriction b flags) then
let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in
- if not (eq_constr cM cM') then
+ if not (eq_constr sigma cM cM') then
unirec_rec curenvnb pb b wt substn cM' cN
else
let cN' = do_reduce flags.modulo_delta curenvnb sigma cN in
- if not (eq_constr cN cN') then
+ if not (eq_constr sigma cN cN') then
unirec_rec curenvnb pb b wt substn cM cN'
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -1500,7 +1500,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
let return a b =
let (evd,c as a) = a () in
- if List.exists (fun (evd',c') -> eq_constr c c') b then b else a :: b
+ if List.exists (fun (evd',c') -> eq_constr evd' c c') b then b else a :: b
in
let fail str _ = error str in
let bind f g a =
@@ -1577,7 +1577,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
in
if not flags.allow_K_in_toplevel_higher_order_unification &&
(* ensure we found a different instance *)
- List.exists (fun op -> eq_constr op cl) l
+ List.exists (fun op -> eq_constr evd op cl) l
then error_non_linear_unification env evd hdmeta cl
else (evd',cl::l)
else if flags.allow_K_in_toplevel_higher_order_unification
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 20:32:06 +0000