From 6dceb3df36d30ad32db7e73713e7f7dee083e872 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 24 Oct 2006 12:55:46 +0000
Subject: Extension de la primitive ltac fresh pour qu'elle accepte une liste
 de noms et de chaînes qu'elle va concaténer pour créer un nom.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9267 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 1dc822a27c..662b268f64 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -234,7 +234,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg =
       'ref * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list
   | TacExternal of loc * string * string * 
       ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg list
-  | TacFreshId     of string option
+  | TacFreshId     of string or_var list
   | Tacexp of 'tac
 
 (* Globalized tactics *)
-- 
cgit v1.2.3