Correction bug #1041 (double cause : non évitement des noms existants en

cas de création de nom par défaut; utilisation de _ comme nom dans evarutil.ml)
+ test régression bug #1041 + allègement syntaxe tactique evar
+ essai de ne pas faire dépendre les evars des variables anonymes afin
  de résoudre le bug #932


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

1 files changed, 11 insertions, 0 deletions

diff --git a/test-suite/success/instantiate.v b/test-suite/success/instantiate.v
new file mode 100644
index 000000000..4224405d9
--- /dev/null
+++ b/test-suite/success/instantiate.v
@@ -0,0 +1,11 @@
+(* Test régression bug #1041 *)
+
+Goal Prop.
+
+pose (P:= fun x y :Prop => y).
+evar (Q: forall X Y,P X Y -> Prop) .
+
+instantiate (1:= fun _ => _ ) in (Value of Q).
+instantiate (1:= fun _ => _ ) in (Value of Q).
+instantiate (1:= fun _ => _ ) in (Value of Q).
+instantiate (1:= H) in (Value of Q).