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

4 files changed, 38 insertions, 20 deletions

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 9bf5d0ea90..2e72784b5f 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -115,7 +115,10 @@ GEXTEND Gram
   ;
   may_eval_arg:
     [ [ c = constr_eval -> ConstrMayEval c
-      | IDENT "fresh"; s = OPT STRING -> TacFreshId s ] ]
+      | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l ] ]
+  ;
+  fresh_id:
+    [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (loc,id) ] ]
   ;
   constr_eval:
     [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index f354ac44f3..fdb0ff5032 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -127,6 +127,8 @@ let rec pr_message_token prid = function
   | MsgInt n -> int n
   | MsgIdent id -> prid id
 
+let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s)
+
 let rec pr_raw_generic prc prlc prtac prref (x:(Genarg.rlevel, Tacexpr.raw_tactic_expr) Genarg.generic_argument) =
   match Genarg.genarg_tag x with
   | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false")
@@ -900,7 +902,7 @@ let rec pr_tac inherited tac =
       str "constr:" ++ pr_constr c, latom
   | TacArg(ConstrMayEval c) ->
       pr_may_eval pr_constr pr_lconstr pr_cst c, leval
-  | TacArg(TacFreshId sopt) -> str "fresh" ++ pr_opt qs sopt, latom
+  | TacArg(TacFreshId l) -> str "fresh" ++ pr_fresh_ids l, latom
   | TacArg(Integer n) -> int n, latom
   | TacArg(TacCall(loc,f,l)) ->
       pr_with_comments loc
@@ -921,7 +923,7 @@ and pr_tacarg = function
   | Reference r -> pr_ref r
   | ConstrMayEval c ->
       pr_may_eval pr_constr pr_lconstr pr_cst c
-  | TacFreshId sopt -> str "fresh" ++ pr_opt qs sopt
+  | TacFreshId l -> str "fresh" ++ pr_fresh_ids l
   | TacExternal (_,com,req,la) ->
       str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++ 
       spc() ++ prlist_with_sep spc pr_tacarg la
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 *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f48e7935cb..f7e4a97506 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -223,7 +223,7 @@ let _ =
       (fun (s,t) -> add_primitive_tactic s t)
       [ "idtac",TacId [];
         "fail", TacFail(ArgArg 0,[]);
-        "fresh", TacArg(TacFreshId None)
+        "fresh", TacArg(TacFreshId [])
       ]
  
 let lookup_atomic id = Idmap.find id !atomic_mactab
@@ -369,9 +369,9 @@ let intern_hyp ist (loc,id as locid) =
 
 let intern_hyp_or_metaid ist id = intern_hyp ist (skip_metaid id)
 
-let intern_int_or_var ist = function
+let intern_or_var ist = function
   | ArgVar locid -> ArgVar (intern_hyp ist locid)
-  | ArgArg n as x -> x
+  | ArgArg _ as x -> x
 
 let intern_inductive ist = function
   | Ident (loc,id) when find_var id ist -> ArgVar (loc,id)
@@ -533,7 +533,7 @@ let intern_inversion_strength lf ist = function
 
 (* Interprets an hypothesis name *)
 let intern_hyp_location ist ((occs,id),hl) =
-  ((List.map (intern_int_or_var ist) occs,intern_hyp ist (skip_metaid id)), hl)
+  ((List.map (intern_or_var ist) occs,intern_hyp ist (skip_metaid id)), hl)
 
 let interp_constrpattern_gen sigma env ltacvar c =
   let c = intern_gen false ~allow_soapp:true ~ltacvars:(ltacvar,[])
@@ -663,13 +663,13 @@ let rec intern_atomic lf ist x =
   (* Automation tactics *)
   | TacTrivial (lems,l) -> TacTrivial (List.map (intern_constr ist) lems,l)
   | TacAuto (n,lems,l) ->
-      TacAuto (option_map (intern_int_or_var ist) n,
+      TacAuto (option_map (intern_or_var ist) n,
         List.map (intern_constr ist) lems,l)
   | TacAutoTDB n -> TacAutoTDB n
   | TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id)
   | TacDestructConcl -> TacDestructConcl
   | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
-  | TacDAuto (n,p) -> TacDAuto (option_map (intern_int_or_var ist) n,p)
+  | TacDAuto (n,p) -> TacDAuto (option_map (intern_or_var ist) n,p)
 
   (* Derived basic tactics *)
   | TacSimpleInduction h ->
@@ -767,7 +767,7 @@ and intern_tactic_seq ist = function
       ist.ltacvars, TacMatch (lz,intern_tactic ist c,intern_match_rule ist lmr)
   | TacId l -> ist.ltacvars, TacId (intern_message ist l)
   | TacFail (n,l) -> 
-      ist.ltacvars, TacFail (intern_int_or_var ist n,intern_message ist l)
+      ist.ltacvars, TacFail (intern_or_var ist n,intern_message ist l)
   | TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac)
   | TacAbstract (tac,s) -> ist.ltacvars, TacAbstract (intern_tactic ist tac,s)
   | TacThen (t1,t2) ->
@@ -780,7 +780,7 @@ and intern_tactic_seq ist = function
       lfun',
       TacThens (t, List.map (intern_tactic { ist with ltacvars = lfun' }) tl)
   | TacDo (n,tac) -> 
-      ist.ltacvars, TacDo (intern_int_or_var ist n,intern_tactic ist tac)
+      ist.ltacvars, TacDo (intern_or_var ist n,intern_tactic ist tac)
   | TacTry tac -> ist.ltacvars, TacTry (intern_tactic ist tac)
   | TacInfo tac -> ist.ltacvars, TacInfo (intern_tactic ist tac)
   | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_tactic ist tac)
@@ -815,7 +815,7 @@ and intern_tacarg strict ist = function
         List.map (intern_tacarg !strict_check ist) l)
   | TacExternal (loc,com,req,la) -> 
       TacExternal (loc,com,req,List.map (intern_tacarg !strict_check ist) la)
-  | TacFreshId _ as x -> x
+  | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x)
   | Tacexp t -> Tacexp (intern_tactic ist t)
   | TacDynamic(loc,t) as x ->
       (match tag t with
@@ -842,7 +842,7 @@ and intern_genarg ist x =
   | IntArgType -> in_gen globwit_int (out_gen rawwit_int x)
   | IntOrVarArgType ->
       in_gen globwit_int_or_var
-        (intern_int_or_var ist (out_gen rawwit_int_or_var x))
+        (intern_or_var ist (out_gen rawwit_int_or_var x))
   | StringArgType ->
       in_gen globwit_string (out_gen rawwit_string x)
   | PreIdentArgType ->
@@ -1219,11 +1219,25 @@ let rec intropattern_ids = function
       List.flatten (List.map intropattern_ids (List.flatten ll))
   | IntroWildcard | IntroAnonymous -> []
 
-let rec extract_ids = function
-  | (id,VIntroPattern ipat)::tl -> intropattern_ids ipat @ extract_ids tl
-  | _::tl -> extract_ids tl
+let rec extract_ids ids = function
+  | (id,VIntroPattern ipat)::tl when not (List.mem id ids) ->
+      intropattern_ids ipat @ extract_ids ids tl
+  | _::tl -> extract_ids ids tl
   | [] -> []
 
+let default_fresh_id = id_of_string "H"
+
+let interp_fresh_id ist gl l =
+  let ids = map_succeed (function ArgVar(_,id) -> id | _ -> failwith "") l in
+  let avoid = extract_ids ids ist.lfun in
+  let id = 
+    if l = [] then default_fresh_id 
+    else
+      id_of_string (String.concat "" (List.map (function
+	| ArgArg s -> s
+	| ArgVar (_,id) -> string_of_id (interp_ident ist gl id)) l)) in 
+  Tactics.fresh_id avoid id gl
+
 (* To retype a list of key*constr with undefined key *)
 let retype_list sigma env lst =
   List.fold_right (fun (x,csr) a ->
@@ -1561,9 +1575,8 @@ and interp_tacarg ist gl = function
       interp_app ist gl fv largs loc
   | TacExternal (loc,com,req,la) ->
       interp_external loc ist gl com req (List.map (interp_tacarg ist gl) la)
-  | TacFreshId idopt -> 
-      let s = match idopt with None -> "H" | Some s -> s in
-      let id = Tactics.fresh_id (extract_ids ist.lfun) (id_of_string s) gl in
+  | TacFreshId l -> 
+      let id = interp_fresh_id ist gl l in
       VIntroPattern (IntroIdentifier id)
   | Tacexp t -> val_interp ist gl t
   | TacDynamic(_,t) ->