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.

1 files changed, 7 insertions, 0 deletions

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.