From 35fb7ad402fee1e3e247ccf37438d3a7a5230629 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 29 May 2016 15:58:21 +0200
Subject: 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.
---
 tactics/tactics.ml            |  2 ++
 test-suite/bugs/closed/4746.v | 14 ++++++++++++++
 2 files changed, 16 insertions(+)
 create mode 100644 test-suite/bugs/closed/4746.v

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.
-- 
cgit v1.2.3