diff options
Diffstat (limited to 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 2113ae89..c7e1db60 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pptactic.ml 8926 2006-06-08 20:23:17Z herbelin $ *) +(* $Id: pptactic.ml 9319 2006-10-30 12:41:21Z barras $ *) open Pp open Names @@ -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") @@ -261,8 +263,6 @@ let rec pr_tacarg_using_rule pr_gen = function | [], [] -> mt () | _ -> failwith "Inconsistent arguments of extended tactic" -let surround p = hov 1 (str"(" ++ p ++ str")") - let pr_extend_gen prgen lev s l = try let tags = List.map genarg_tag l in @@ -521,11 +521,11 @@ let rec pr_tacarg_using_rule pr_gen = function let pr_then () = str ";" let ltop = (5,E) -let lseq = 5 +let lseq = 4 let ltactical = 3 let lorelse = 2 -let llet = 1 -let lfun = 1 +let llet = 5 +let lfun = 5 let lcomplete = 1 let labstract = 3 let lmatch = 1 @@ -533,6 +533,7 @@ let latom = 0 let lcall = 1 let leval = 1 let ltatom = 1 +let linfo = 5 let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq @@ -875,7 +876,7 @@ let rec pr_tac inherited tac = ltactical | TacInfo t -> hov 1 (str "info" ++ spc () ++ pr_tac (ltactical,E) t), - ltactical + linfo | TacOrelse (t1,t2) -> hov 1 (pr_tac (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++ pr_tac (lorelse,E) t2), @@ -902,7 +903,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 @@ -923,7 +924,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 |