diff options
| -rw-r--r-- | pretyping/unification.ml | 9 | ||||
| -rw-r--r-- | pretyping/unification.mli | 1 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 1 | ||||
| -rw-r--r-- | tactics/auto.ml | 1 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 1 | ||||
| -rw-r--r-- | tactics/equality.ml | 1 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 1 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2123.v | 11 | ||||
| -rw-r--r-- | test-suite/success/apply.v | 7 |
10 files changed, 34 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 8ea2eae11..0846359a8 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -128,6 +128,7 @@ type unify_flags = { use_metas_eagerly : bool; modulo_delta : Names.transparent_state; resolve_evars : bool; + use_evars_pattern_unification : bool } let default_unify_flags = { @@ -135,6 +136,7 @@ let default_unify_flags = { use_metas_eagerly = true; modulo_delta = full_transparent_state; resolve_evars = false; + use_evars_pattern_unification = true; } let default_no_delta_unify_flags = { @@ -142,6 +144,7 @@ let default_no_delta_unify_flags = { use_metas_eagerly = true; modulo_delta = empty_transparent_state; resolve_evars = false; + use_evars_pattern_unification = true; } let expand_key env = function @@ -229,12 +232,14 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag (unirec_rec curenvnb topconv true substn p1 p2) c1 c2) cl1 cl2 | App (f1,l1), _ when - isMeta f1 & is_unification_pattern curenvnb f1 l1 cN & + (isMeta f1 || flags.use_evars_pattern_unification && isEvar 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 & is_unification_pattern curenvnb f2 l2 cM & + (isMeta f2 || flags.use_evars_pattern_unification && isEvar 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 8d71ec4bd..43c9dd2e9 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -19,6 +19,7 @@ type unify_flags = { use_metas_eagerly : bool; modulo_delta : Names.transparent_state; resolve_evars : bool; + use_evars_pattern_unification : bool } val default_unify_flags : unify_flags diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index c3e6e3d87..87dd26779 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -109,6 +109,7 @@ let fail_quick_unif_flags = { use_metas_eagerly = false; modulo_delta = empty_transparent_state; resolve_evars = false; + use_evars_pattern_unification = false; } (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) diff --git a/tactics/auto.ml b/tactics/auto.ml index 8a2578c30..407733e68 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -709,6 +709,7 @@ let auto_unif_flags = { use_metas_eagerly = false; modulo_delta = empty_transparent_state; resolve_evars = true; + use_evars_pattern_unification = false; } (* Try unification with the precompiled clause, then use registered Apply *) diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 6baedb76a..2b9a48030 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -104,6 +104,7 @@ let auto_unif_flags = { use_metas_eagerly = true; modulo_delta = var_full_transparent_state; resolve_evars = false; + use_evars_pattern_unification = true; } let unify_e_resolve flags (c,clenv) gls = diff --git a/tactics/equality.ml b/tactics/equality.ml index dcb2d6037..89a3704ee 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -66,6 +66,7 @@ let rewrite_unif_flags = { Unification.use_metas_eagerly = true; Unification.modulo_delta = empty_transparent_state; Unification.resolve_evars = true; + Unification.use_evars_pattern_unification = true; } let side_tac tac sidetac = diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 6da110139..52f10d46c 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -283,6 +283,7 @@ let rewrite_unif_flags = { Unification.use_metas_eagerly = true; Unification.modulo_delta = empty_transparent_state; Unification.resolve_evars = true; + Unification.use_evars_pattern_unification = true; } let conv_transparent_state = (Idpred.empty, Cpred.full) @@ -292,6 +293,7 @@ let rewrite2_unif_flags = { Unification.use_metas_eagerly = true; Unification.modulo_delta = empty_transparent_state; Unification.resolve_evars = true; + Unification.use_evars_pattern_unification = true; } let setoid_rewrite_unif_flags = { @@ -299,6 +301,7 @@ let setoid_rewrite_unif_flags = { Unification.use_metas_eagerly = true; Unification.modulo_delta = conv_transparent_state; Unification.resolve_evars = true; + Unification.use_evars_pattern_unification = true; } let convertible env evd x y = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3cd819947..e96806de1 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -681,6 +681,7 @@ let elim_flags = { use_metas_eagerly = true; modulo_delta = empty_transparent_state; resolve_evars = false; + use_evars_pattern_unification = true; } let elimination_clause_scheme with_evars allow_K elimclause indclause gl = diff --git a/test-suite/bugs/closed/shouldsucceed/2123.v b/test-suite/bugs/closed/shouldsucceed/2123.v new file mode 100644 index 000000000..422a2c126 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2123.v @@ -0,0 +1,11 @@ +(* About the detection of non-dependent metas by the refine tactic *) + +(* The following is a simplification of bug #2123 *) + +Parameter fset : nat -> Set. +Parameter widen : forall (n : nat) (s : fset n), { x : fset (S n) | s=s }. +Goal forall i, fset (S i). +intro. +refine (proj1_sig (widen i _)). + + diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 4f47702c6..f95352b65 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -277,3 +277,10 @@ try eapply ex_intro. trivial. Qed. +(* Check pattern-unification on evars in apply unification *) + +Lemma evar : exists f : nat -> nat, forall x, f x = 0 -> x = 0. +Proof. +eexists; intros x H. +apply H. +Qed. |