aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/evd.ml8
-rw-r--r--pretyping/evd.mli4
-rw-r--r--pretyping/unification.ml23
-rw-r--r--pretyping/unification.mli1
-rw-r--r--proofs/clenvtac.ml1
-rw-r--r--tactics/auto.ml1
-rw-r--r--tactics/class_tactics.ml41
-rw-r--r--tactics/equality.ml32
-rw-r--r--tactics/rewrite.ml43
-rw-r--r--test-suite/success/unification.v2
10 files changed, 62 insertions, 14 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 9d3e4225db..5125b21cc1 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -495,6 +495,14 @@ let evar_list evd c =
| _ -> fold_constr evrec acc c in
evrec [] c
+let collect_evars c =
+ let rec collrec acc c =
+ match kind_of_term c with
+ | Evar (evk,_) -> ExistentialSet.add evk acc
+ | _ -> fold_constr collrec acc c
+ in
+ collrec ExistentialSet.empty c
+
(**********************************************************)
(* Sort variables *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index c0efdb9f82..8131837d81 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -200,8 +200,6 @@ val evar_source : existential_key -> evar_map -> hole_kind located
[evar_merge evd ev1] extends the evars of [evd] with [evd1] *)
val evar_merge : evar_map -> evar_map -> evar_map
-val evar_list : evar_map -> constr -> existential list
-
(** Unification constraints *)
type conv_pb = Reduction.conv_pb
type evar_constraint = conv_pb * env * constr * constr
@@ -214,6 +212,8 @@ val extract_changed_conv_pbs : evar_map ->
evar_map * evar_constraint list
val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
+val evar_list : evar_map -> constr -> existential list
+val collect_evars : constr -> ExistentialSet.t
(** Metas *)
val find_meta : evar_map -> metavariable -> clbinding
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 47fec14963..d09e5f2451 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -163,6 +163,7 @@ type unify_flags = {
modulo_delta_types : Names.transparent_state;
resolve_evars : bool;
use_evars_pattern_unification : bool;
+ frozen_evars : ExistentialSet.t;
modulo_betaiota : bool;
modulo_eta : bool;
allow_K_in_toplevel_higher_order_unification : bool
@@ -175,6 +176,7 @@ let default_unify_flags = {
modulo_delta_types = full_transparent_state;
resolve_evars = false;
use_evars_pattern_unification = true;
+ frozen_evars = ExistentialSet.empty;
modulo_betaiota = false;
modulo_eta = true;
allow_K_in_toplevel_higher_order_unification = false
@@ -187,6 +189,7 @@ let default_no_delta_unify_flags = {
modulo_delta_types = full_transparent_state;
resolve_evars = false;
use_evars_pattern_unification = false;
+ frozen_evars = ExistentialSet.empty;
modulo_betaiota = false;
modulo_eta = true;
allow_K_in_toplevel_higher_order_unification = false
@@ -199,6 +202,7 @@ let elim_flags = {
modulo_delta_types = full_transparent_state;
resolve_evars = false;
use_evars_pattern_unification = true;
+ frozen_evars = ExistentialSet.empty;
modulo_betaiota = false;
modulo_eta = true;
allow_K_in_toplevel_higher_order_unification = true
@@ -211,6 +215,7 @@ let elim_no_delta_flags = {
modulo_delta_types = full_transparent_state;
resolve_evars = false;
use_evars_pattern_unification = false;
+ frozen_evars = ExistentialSet.empty;
modulo_betaiota = false;
modulo_eta = true;
allow_K_in_toplevel_higher_order_unification = true
@@ -251,6 +256,10 @@ let do_reduce env sigma c =
let (t, l) = whd_betaiota_deltazeta_for_iota_state env sigma (c, empty_stack) in
applist (t, list_of_stack l)
+let isAllowedEvar flags c = match kind_of_term c with
+ | Evar (evk,_) -> not (ExistentialSet.mem evk flags.frozen_evars)
+ | _ -> false
+
let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n =
let rec unirec_rec (curenv,nb as curenvnb) pb b ((sigma,metasubst,evarsubst) as substn) curm curn =
let cM = Evarutil.whd_head_evar sigma curm
@@ -280,8 +289,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
(sigma,(k,lift (-nb) cM,fst (extract_instance_status pb))::metasubst,
evarsubst)
else error_cannot_unify_local curenv sigma (m,n,cM)
- | Evar ev, _ -> sigma,metasubst,((curenv, ev,cN)::evarsubst)
- | _, Evar ev -> sigma,metasubst,((curenv, ev,cM)::evarsubst)
+ | Evar (evk,_ as ev), _
+ when not (ExistentialSet.mem evk flags.frozen_evars) ->
+ sigma,metasubst,((curenv, ev,cN)::evarsubst)
+ | _, Evar (evk,_ as ev)
+ when not (ExistentialSet.mem evk flags.frozen_evars) ->
+ sigma,metasubst,((curenv, ev,cM)::evarsubst)
| Sort s1, Sort s2 ->
(try
@@ -318,13 +331,15 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
reduce curenvnb pb b substn cM cN)
| App (f1,l1), _ when
- (isMeta f1 || use_evars_pattern_unification flags && isEvar f1) &
+ (isMeta f1 || use_evars_pattern_unification flags &&
+ isAllowedEvar flags f1) &
is_unification_pattern curenvnb f1 l1 cN &
not (dependent f1 cN) ->
solve_pattern_eqn_array curenvnb f1 l1 cN substn
| _, App (f2,l2) when
- (isMeta f2 || use_evars_pattern_unification flags && isEvar f2) &
+ (isMeta f2 || use_evars_pattern_unification flags &&
+ isAllowedEvar flags f2) &
is_unification_pattern curenvnb f2 l2 cM &
not (dependent f2 cM) ->
solve_pattern_eqn_array curenvnb f2 l2 cM substn
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 0f7eec6925..aa0267698e 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -17,6 +17,7 @@ type unify_flags = {
modulo_delta_types : Names.transparent_state;
resolve_evars : bool;
use_evars_pattern_unification : bool;
+ frozen_evars : ExistentialSet.t;
modulo_betaiota : bool;
modulo_eta : bool;
allow_K_in_toplevel_higher_order_unification : bool
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index e056519523..dad4b5041e 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -107,6 +107,7 @@ let fail_quick_unif_flags = {
modulo_delta_types = full_transparent_state;
resolve_evars = false;
use_evars_pattern_unification = false;
+ frozen_evars = ExistentialSet.empty;
modulo_betaiota = false;
modulo_eta = true;
allow_K_in_toplevel_higher_order_unification = false
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4c00a60d00..6780ae2fcf 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -845,6 +845,7 @@ let auto_unif_flags = {
modulo_delta_types = full_transparent_state;
resolve_evars = true;
use_evars_pattern_unification = false;
+ frozen_evars = ExistentialSet.empty;
modulo_betaiota = false;
modulo_eta = true;
allow_K_in_toplevel_higher_order_unification = false
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 3b193f6d93..3f4e773eca 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -79,6 +79,7 @@ let auto_unif_flags = {
modulo_delta_types = full_transparent_state;
resolve_evars = false;
use_evars_pattern_unification = true;
+ frozen_evars = ExistentialSet.empty;
modulo_betaiota = true;
modulo_eta = true;
allow_K_in_toplevel_higher_order_unification = false
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3b734b4c64..f6e8837f8b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -87,12 +87,25 @@ let rewrite_unif_flags = {
Unification.modulo_delta_types = empty_transparent_state;
Unification.resolve_evars = true;
Unification.use_evars_pattern_unification = true;
+ Unification.frozen_evars = ExistentialSet.empty;
Unification.modulo_betaiota = false;
Unification.modulo_eta = true;
Unification.allow_K_in_toplevel_higher_order_unification = false
(* allow_K does not matter in practice because calls w_typed_unify *)
}
+let freeze_initial_evars sigma flags clause =
+ (* We take evars of the type: this may include old evars! For excluding *)
+ (* all old evars, including the ones occurring in the rewriting lemma, *)
+ (* we would have to take the clenv_value *)
+ let newevars = Evd.collect_evars (clenv_type clause) in
+ let evars =
+ fold_undefined (fun evk _ evars ->
+ if ExistentialSet.mem evk newevars then evars
+ else ExistentialSet.add evk evars)
+ sigma ExistentialSet.empty in
+ { flags with Unification.frozen_evars = evars }
+
let side_tac tac sidetac =
match sidetac with
| None -> tac
@@ -110,8 +123,9 @@ let instantiate_lemma_all env sigma gl c ty l l2r concl =
let try_occ (evd', c') =
clenv_pose_dependent_evars true {eqclause with evd = evd'}
in
+ let flags = freeze_initial_evars sigma rewrite_unif_flags eqclause in
let occs =
- Unification.w_unify_to_subterm_all ~flags:rewrite_unif_flags env
+ Unification.w_unify_to_subterm_all ~flags env
((if l2r then c1 else c2),concl) eqclause.evd
in List.map try_occ occs
@@ -129,20 +143,22 @@ let rewrite_conv_closed_unif_flags = {
Unification.modulo_delta_types = full_transparent_state;
Unification.resolve_evars = false;
Unification.use_evars_pattern_unification = true;
+ Unification.frozen_evars = ExistentialSet.empty;
Unification.modulo_betaiota = false;
Unification.modulo_eta = true;
Unification.allow_K_in_toplevel_higher_order_unification = false
}
-let rewrite_elim with_evars c e =
- general_elim_clause_gen
- (elimination_clause_scheme with_evars ~flags:rewrite_conv_closed_unif_flags)
- c e
+let rewrite_elim with_evars c e gl =
+ let flags =
+ freeze_initial_evars (project gl) rewrite_conv_closed_unif_flags c in
+ general_elim_clause_gen (elimination_clause_scheme with_evars ~flags) c e gl
-let rewrite_elim_in with_evars id c e =
+let rewrite_elim_in with_evars id c e gl =
+ let flags =
+ freeze_initial_evars (project gl) rewrite_conv_closed_unif_flags c in
general_elim_clause_gen
- (elimination_in_clause_scheme with_evars
- ~flags:rewrite_conv_closed_unif_flags id) c e
+ (elimination_in_clause_scheme with_evars ~flags id) c e gl
(* Ad hoc asymmetric general_elim_clause *)
let general_elim_clause with_evars cls rew elim =
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 41ed88d2f7..b8ebf84a61 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -307,6 +307,7 @@ let rewrite_unif_flags = {
Unification.modulo_delta_types = full_transparent_state;
Unification.resolve_evars = true;
Unification.use_evars_pattern_unification = true;
+ Unification.frozen_evars = ExistentialSet.empty;
Unification.modulo_betaiota = false;
Unification.modulo_eta = true;
Unification.allow_K_in_toplevel_higher_order_unification = true
@@ -319,6 +320,7 @@ let rewrite2_unif_flags =
Unification.modulo_delta_types = conv_transparent_state;
Unification.resolve_evars = true;
Unification.use_evars_pattern_unification = true;
+ Unification.frozen_evars = ExistentialSet.empty;
Unification.modulo_betaiota = true;
Unification.modulo_eta = true;
Unification.allow_K_in_toplevel_higher_order_unification = true
@@ -332,6 +334,7 @@ let general_rewrite_unif_flags () =
Unification.modulo_delta_types = ts;
Unification.resolve_evars = true;
Unification.use_evars_pattern_unification = true;
+ Unification.frozen_evars = ExistentialSet.empty;
Unification.modulo_betaiota = true;
Unification.modulo_eta = true;
Unification.allow_K_in_toplevel_higher_order_unification = true }
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index e5b6e41598..18ba0fc870 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -90,12 +90,14 @@ intros.
apply H.
Qed.
+(* Feature deactivated in commit 14189 (see commit log)
(* Test instanciation of evars by unification *)
Goal (forall x, 0 + x = 0 -> True) -> True.
intros; eapply H.
rewrite <- plus_n_Sm. (* should refine ?x with S ?x' *)
Abort.
+*)
(* Check handling of identity equation between evars *)
(* The example failed to pass until revision 10623 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 03:45:31 +0000