diff options
| author | herbelin | 2006-10-24 12:55:46 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-24 12:55:46 +0000 |
| commit | 6dceb3df36d30ad32db7e73713e7f7dee083e872 (patch) | |
| tree | a929ebb6ad7aae06b05c32b1515db924f4761d5f /parsing | |
| parent | f1248d64c25602d75d069b07b51a8b4f751415b2 (diff) | |
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
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_ltac.ml4 | 5 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 6 |
2 files changed, 8 insertions, 3 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 |