From c4f270f573360e39bd91e3ffff8d37775b2871d7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 3 Nov 2014 15:23:57 +0100
Subject: Subtle swap of lines to preserve VarInstance src field before
 checking for residual unifiable evars (otherwise "thin" from logic.ml, erases
 the src field) + typo.

---
 tactics/tactics.ml            | 3 +--
 test-suite/success/destruct.v | 7 +++++++
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5918cf997c..e26be98b53 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3841,11 +3841,10 @@ let pose_induction_arg_then clear_flag isrec with_evars
           let (sigma,c) = use_bindings env sigma elim (c0,lbind) t0 in
           let t = Retyping.get_type_of env sigma c in
           mkletin_goal env sigma with_eq false (id,lastlhyp,ccl,c) (Some t));
+        Proofview.(if with_evars then shelve_unifiable else guard_no_unifiable);
         if is_arg_pure_hyp
         then Tacticals.New.tclTRY (Proofview.V82.tactic (thin [destVar c0]))
         else Proofview.tclUNIT ();
-        Proofview.(if with_evars then shelve_unifiable else guard_no_unifiable);
-        Proofview.shelve_unifiable;
         if isrec then Proofview.cycle (-1) else Proofview.tclUNIT ()
       ])
       (tac fixedvars)
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 0faaa275f2..8e9be2e403 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -369,3 +369,10 @@ intros.
 destruct (H _).
 change (0=0) in H0. (* Check generalization on H0 was made *)
 Abort.
+
+(* Check absence of anomaly (failed at some time) *)
+
+Goal forall A (a:A) (P Q:A->Prop), (forall a, P a -> Q a) -> True.
+intros.
+Fail destruct H.
+Abort.
-- 
cgit v1.2.3