aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/evarconv.ml8
-rw-r--r--pretyping/evarsolve.ml11
-rw-r--r--pretyping/evd.ml21
-rw-r--r--pretyping/evd.mli13
-rw-r--r--pretyping/unification.ml8
-rw-r--r--proofs/clenv.ml4
-rw-r--r--tactics/class_tactics.ml3
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--tactics/tactics.ml18
-rw-r--r--toplevel/himsg.ml4
10 files changed, 55 insertions, 37 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index c436fed2c..f8e959075 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 evd c term) subst in
+ let subst' = List.filter (fun (id,c) -> Term.eq_constr 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 !evdref c t then f k
+ if e_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 evd a term2 || isEvar a)
+ && List.for_all (fun a -> Term.eq_constr 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 evd a term1 || isEvar a)
+ && List.for_all (fun a -> Term.eq_constr 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 4bffe3d1f..ba877d35c 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -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 sigma a c) sub then
+ if List.exists (fun (c,_,_) -> Term.eq_constr 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 sigma y c' then id
+ if Term.eq_constr 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 sigma yc cc -> id
- | _ -> if eq_constr sigma yc c then id else raise Not_found
+ | Some cc when Term.eq_constr yc cc -> id
+ | _ -> if Term.eq_constr 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,8 @@ 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 evd) argsv1 argsv2 then evd else
+ let evdref = ref evd in
+ if Array.equal (e_eq_constr evdref) argsv1 argsv2 then !evdref 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 bd105c728..e49ed7b45 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1333,24 +1333,35 @@ 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_constr evd t u =
+ let b, c = Universes.eq_constr_univs_infer evd.universes.uctx_universes t u in
+ if b then
+ try let evd' = add_universe_constraints evd c in evd', b
+ with Univ.UniverseInconsistency _ -> evd, false
+ else evd, b
+
+let e_eq_constr evdref t u =
+ let evd, b = eq_constr !evdref t u in
+ evdref := evd; b
+
+let eq_constr_test evd t u =
+ snd (eq_constr evd 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
+ Id.equal i1 i2 && Option.equal (eq_constr_test d) c1 c2 && (eq_constr_test 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
+| Evar_defined t1, Evar_defined t2 -> eq_constr_test d t1 t2
| _ -> false
let eq_evar_info d ei1 ei2 =
ei1 == ei2 ||
- eq_constr d ei1.evar_concl ei2.evar_concl &&
+ eq_constr_test 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 *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index d0a47fe96..b284bd42c 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -515,11 +515,18 @@ val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map ->
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
+(** This one forgets about the assignemts of universes. *)
+
+val eq_constr : evar_map -> constr -> constr -> evar_map * bool
+(** Syntactic equality up to universes, recording the associated constraints *)
+
+val e_eq_constr : evar_map ref -> constr -> constr -> bool
+(** Syntactic equality up to universes. *)
-(** Syntactic equality up to universe constraints. *)
-val eq_constr : evar_map -> constr -> constr -> bool
+val eq_constr_test : evar_map -> constr -> constr -> bool
+(** Syntactic equality up to universes, throwing away the (consistent) constraints
+ in case of success. *)
(********************************************************************
constr with holes *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 7530ced7c..7b302229b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -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 sigma cM cM') then
+ if not (Term.eq_constr 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 sigma cN cN') then
+ if not (Term.eq_constr 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 evd' c c') b then b else a :: b
+ if List.exists (fun (evd',c') -> Term.eq_constr 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 evd op cl) l
+ List.exists (fun op -> Term.eq_constr 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
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 5a7572eb2..3ef346634 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -167,7 +167,7 @@ let clenv_assign mv rhs clenv =
error "clenv_assign: circularity in unification";
try
if meta_defined clenv.evd mv then
- if not (eq_constr clenv.evd (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
+ if not (Term.eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
error_incompatible_inst clenv mv
else
clenv
@@ -480,7 +480,7 @@ let clenv_match_args bl clenv =
(fun clenv (loc,b,c) ->
let k = meta_of_binder clenv loc mvs b in
if meta_defined clenv.evd k then
- if eq_constr clenv.evd (fst (meta_fvalue clenv.evd k)).rebus c then clenv
+ if Term.eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
else error_already_defined b
else
clenv_assign_binding clenv k c)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 881bb5c62..35889462b 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -278,14 +278,13 @@ let pf_filtered_hyps gls =
Goal.V82.hyps gls.Evd.sigma (sig_it gls)
let make_hints g st only_classes sign =
- let sigma = project g in
let paths, hintlist =
List.fold_left
(fun (paths, hints) hyp ->
let consider =
try let (_, b, t) = Global.lookup_named (pi1 hyp) in
(* Section variable, reindex only if the type changed *)
- not (eq_constr sigma t (pi3 hyp))
+ not (Term.eq_constr t (pi3 hyp))
with Not_found -> true
in
if consider then
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index c1e6f42f1..51ca5ddda 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -780,7 +780,7 @@ END
let eq_constr x y =
Proofview.Goal.enter (fun gl ->
let evd = Proofview.Goal.sigma gl in
- if Evd.eq_constr evd x y then Proofview.tclUNIT ()
+ if Evd.eq_constr_test evd x y then Proofview.tclUNIT ()
else Tacticals.New.tclFAIL 0 (str "Not equal"))
TACTIC EXTEND constr_eq
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 28e0b7262..08cf95432 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1124,7 +1124,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in
let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
let new_hyp_typ = clenv_type elimclause'' in
- if eq_constr sigma hyp_typ new_hyp_typ then
+ if Term.eq_constr hyp_typ new_hyp_typ then
errorlabstrm "general_rewrite_in"
(str "Nothing to rewrite in " ++ pr_id id ++ str".");
clenv_refine_in with_evars id id sigma elimclause''
@@ -3065,14 +3065,14 @@ let specialize_eqs id gl =
match kind_of_term ty with
| Prod (na, t, b) ->
(match kind_of_term t with
- | App (eq, [| eqty; x; y |]) when eq_constr !evars (Lazy.force coq_eq) eq ->
+ | App (eq, [| eqty; x; y |]) when Term.eq_constr (Lazy.force coq_eq) eq ->
let c = if noccur_between 1 (List.length ctx) x then y else x in
let pt = mkApp (Lazy.force coq_eq, [| eqty; c; c |]) in
let p = mkApp (Lazy.force coq_eq_refl, [| eqty; c |]) in
if unif (push_rel_context ctx env) evars pt t then
aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
else acc, in_eqs, ctx, ty
- | App (heq, [| eqty; x; eqty'; y |]) when eq_constr !evars heq (Lazy.force coq_heq) ->
+ | App (heq, [| eqty; x; eqty'; y |]) when Term.eq_constr heq (Lazy.force coq_heq) ->
let eqt, c = if noccur_between 1 (List.length ctx) x then eqty', y else eqty, x in
let pt = mkApp (Lazy.force coq_heq, [| eqt; c; eqt; c |]) in
let p = mkApp (Lazy.force coq_heq_refl, [| eqt; c |]) in
@@ -4032,8 +4032,8 @@ let intros_transitivity n = Tacticals.New.tclTHEN intros (transitivity_gen n)
(** d1 is the section variable in the global context, d2 in the goal context *)
let interpretable_as_section_decl evd d1 d2 = match d2,d1 with
| (_,Some _,_), (_,None,_) -> false
- | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr evd b1 b2 && eq_constr evd t1 t2
- | (_,None,t1), (_,_,t2) -> eq_constr evd t1 t2
+ | (_,Some b1,t1), (_,Some b2,t2) -> e_eq_constr evd b1 b2 && e_eq_constr evd t1 t2
+ | (_,None,t1), (_,_,t2) -> e_eq_constr evd t1 t2
let abstract_subproof id gk tac =
let open Tacticals.New in
@@ -4042,25 +4042,25 @@ let abstract_subproof id gk tac =
Proofview.Goal.nf_enter begin fun gl ->
let current_sign = Global.named_context()
and global_sign = Proofview.Goal.hyps gl in
- let sigma = Proofview.Goal.sigma gl in
+ let evdref = ref (Proofview.Goal.sigma gl) in
let sign,secsign =
List.fold_right
(fun (id,_,_ as d) (s1,s2) ->
if mem_named_context id current_sign &&
- interpretable_as_section_decl sigma (Context.lookup_named id current_sign) d
+ interpretable_as_section_decl evdref (Context.lookup_named id current_sign) d
then (s1,push_named_context_val d s2)
else (add_named_decl d s1,s2))
global_sign (empty_named_context,empty_named_context_val) in
let id = next_global_ident_away id (pf_ids_of_hyps gl) in
let concl = it_mkNamedProd_or_LetIn (Proofview.Goal.concl gl) sign in
let concl =
- try flush_and_check_evars (Proofview.Goal.sigma gl) concl
+ try flush_and_check_evars !evdref concl
with Uninstantiated_evar _ ->
error "\"abstract\" cannot handle existentials." in
let evd, ctx, concl =
(* FIXME: should be done only if the tactic succeeds *)
- let evd, nf = nf_evars_and_universes (Proofview.Goal.sigma gl) in
+ let evd, nf = nf_evars_and_universes !evdref in
let ctx = Evd.universe_context_set evd in
evd, ctx, nf concl
in
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 6994c366c..10b1f48c3 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -277,11 +277,11 @@ let explain_unification_error env sigma p1 p2 = function
| NotSameArgSize | NotSameHead | NoCanonicalStructure ->
(* Error speaks from itself *) mt ()
| ConversionFailed (env,t1,t2) ->
- if eq_constr sigma t1 p1 && eq_constr sigma t2 p2 then mt () else
+ if Term.eq_constr t1 p1 && Term.eq_constr t2 p2 then mt () else
let env = make_all_name_different env in
let t1 = Evarutil.nf_evar sigma t1 in
let t2 = Evarutil.nf_evar sigma t2 in
- if not (eq_constr sigma t1 p1) || not (eq_constr sigma t2 p2) then
+ if not (Term.eq_constr t1 p1) || not (Term.eq_constr t2 p2) then
let t1, t2 = pr_explicit env sigma t1 t2 in
spc () ++ str "(cannot unify " ++ t1 ++ strbrk " and " ++
t2 ++ str ")"
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-29 23:10:53 +0000