Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui

s'est avéré ralentir la compilation des user-contribs au final, sans
compter aussi le bug 1980 apparemment introduit par ce commit).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11505 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 6 deletions

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index dbb0d7e4f..319ed6880 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -224,11 +224,18 @@ intros x H; eapply trans_equal;
 [apply H | unfold x;match goal with |- ?x = ?x => reflexivity end].
 Qed.
 
-  (* This does not work (oct 2008) because "match goal" sees "?evar = O" 
-     and not "O = O"
+(* Test non-regression of (temporary) bug 1981 *)
 
-Lemma eapply_evar : O=O -> 0=O.
-intro H; eapply trans_equal; 
-  [apply H | match goal with |- ?x = ?x => reflexivity end].
+Goal exists n : nat, True.
+eapply ex_intro.
+exact O.
+trivial.
+Qed.
+
+(* Test non-regression of (temporary) bug 1980 *)
+
+Goal True.
+try eapply ex_intro.
+trivial.
 Qed.
-*)
+