From 5458617d1b3c6b0a5ff846ef977d3bdaeda9fb4f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 12 Dec 2006 09:38:53 +0000
Subject: 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
---
 tactics/extratactics.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 52fa2a8607..cb67bb2ae5 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -285,7 +285,7 @@ open Evar_tactics
 (* evar creation *)
 
 TACTIC EXTEND evar
-  [ "evar" "(" ident(id) ":" constr(typ) ")" ] -> [ let_evar (Name id) typ ]
+  [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
 | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ]
 END
 
-- 
cgit v1.2.3