diff options
| author | Pierre-Marie Pédrot | 2016-05-29 15:58:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-29 16:12:50 +0200 |
| commit | 35fb7ad402fee1e3e247ccf37438d3a7a5230629 (patch) | |
| tree | 2280a11230b0e51787960eeeb2a36d96c63727c9 | |
| parent | 34ba7e0d17c76c42a8ece4d195d280f7722f3bae (diff) | |
Fix bug #4746: Anomaly: Evar ?X10 was not declared.
Some dubious evarmap manipulation is going on in destruct because of the
use of clenv primitives. Here, building a clenv was introducing new evars
that were not taken into account in the remainder of the tactic. We plug
them back using a local workaround.
Eventually, this code should be replaced by an evar-based one, but meanwhile,
we rely on what is probably a hack.
| -rw-r--r-- | tactics/tactics.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4746.v | 14 |
2 files changed, 16 insertions, 0 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 63d3c694ea..4562e25184 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1224,6 +1224,8 @@ let general_elim with_evars clear_flag (c, lbindc) elim = let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in let elimtac = elimination_clause_scheme with_evars in let indclause = make_clenv_binding env sigma (c, t) lbindc in + let sigma = meta_merge sigma (clear_metas indclause.evd) in + Proofview.Unsafe.tclEVARS sigma <*> Tacticals.New.tclTHEN (general_elim_clause_gen elimtac indclause elim) (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c) diff --git a/test-suite/bugs/closed/4746.v b/test-suite/bugs/closed/4746.v new file mode 100644 index 0000000000..d64cc6fe68 --- /dev/null +++ b/test-suite/bugs/closed/4746.v @@ -0,0 +1,14 @@ +Variables P Q : nat -> Prop. +Variable f : nat -> nat. + +Goal forall (x:nat), (forall y, P y -> forall z, Q z -> y=f z -> False) -> False. +Proof. +intros. +ecase H with (3:=eq_refl). +Abort. + +Goal forall (x:nat), (forall y, y=x -> False) -> False. +Proof. +intros. +unshelve ecase H with (1:=eq_refl). +Qed. |