diff options
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 53 |
1 files changed, 24 insertions, 29 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index b219ee25ca..5e3f4df192 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -22,10 +22,11 @@ open Tactypes open Locus open Decl_kinds open Genredexpr -open Pputils open Ppconstr +open Pputils open Printer +open Genintern open Tacexpr open Tacarg open Tactics @@ -158,8 +159,8 @@ let string_of_genarg_arg (ArgumentType arg) = end | _ -> default - let pr_with_occurrences pr c = pr_with_occurrences pr keyword c - let pr_red_expr pr c = pr_red_expr pr keyword c + let pr_with_occurrences pr c = Ppred.pr_with_occurrences pr keyword c + let pr_red_expr pr c = Ppred.pr_red_expr pr keyword c let pr_may_eval test prc prlc pr2 pr3 = function | ConstrEval (r,c) -> @@ -185,12 +186,6 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_and_short_name pr (c,_) = pr c - let pr_or_by_notation f = CAst.with_val (function - | AN v -> f v - | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc) - - let pr_located pr (_,x) = pr x - let pr_evaluable_reference = function | EvalVarRef id -> pr_id id | EvalConstRef sp -> pr_global (Globnames.ConstRef sp) @@ -234,8 +229,8 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_tacarg_using_rule pr_gen l = let l = match l with | TacTerm s :: l -> - (** First terminal token should be considered as the name of the tactic, - so we tag it differently than the other terminal tokens. *) + (* First terminal token should be considered as the name of the tactic, + so we tag it differently than the other terminal tokens. *) primitive s :: tacarg_using_rule_token pr_gen l | _ -> tacarg_using_rule_token pr_gen l in @@ -294,7 +289,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr _ = str "_" in KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)" - let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.tag arg)) + let pr_farg prtac arg = prtac (1, Any) (TacArg (CAst.make arg)) let is_genarg tag wit = let ArgT.Any tag = tag in @@ -350,9 +345,9 @@ let string_of_genarg_arg (ArgumentType arg) = pr_extend_gen (pr_farg prtac) let pr_raw_alias prtac lev key args = - pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args + pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (CAst.make a)))) lev key args let pr_glob_alias prtac lev key args = - pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args + pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (CAst.make a)))) lev key args (**********************************************************************) (* The tactic printer *) @@ -579,7 +574,7 @@ let pr_goal_selector ~toplevel s = pr_gen arg else str name ++ str ":" ++ surround (pr_gen arg) - | _ -> pr_arg (TacArg (Loc.tag t)) in + | _ -> pr_arg (TacArg (CAst.make t)) in hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++ str " :=" ++ brk (1,1) ++ pr t) @@ -693,7 +688,7 @@ let pr_goal_selector ~toplevel s = (* match t with | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal | _ ->*) - let s = prlist_with_sep spc Ppconstr.pr_lname nal ++ str ":" ++ pr.pr_lconstr t in + let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in spc() ++ hov 1 (str"(" ++ s ++ str")") in let pr_fix_tac (id,n,c) = @@ -1045,30 +1040,30 @@ let pr_goal_selector ~toplevel s = | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom | TacId l -> keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom - | TacAtom (loc,t) -> + | TacAtom { CAst.loc; v=t } -> pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom - | TacArg(_,Tacexp e) -> + | TacArg { CAst.v=Tacexp e } -> pr_tac inherited e, latom - | TacArg(_,ConstrMayEval (ConstrTerm c)) -> + | TacArg { CAst.v=ConstrMayEval (ConstrTerm c) } -> keyword "constr:" ++ pr.pr_constr c, latom - | TacArg(_,ConstrMayEval c) -> + | TacArg { CAst.v=ConstrMayEval c } -> pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval - | TacArg(_,TacFreshId l) -> + | TacArg { CAst.v=TacFreshId l } -> primitive "fresh" ++ pr_fresh_ids l, latom - | TacArg(_,TacGeneric arg) -> + | TacArg { CAst.v=TacGeneric arg } -> pr.pr_generic arg, latom - | TacArg(_,TacCall(_,(f,[]))) -> + | TacArg { CAst.v=TacCall {CAst.v=(f,[])} } -> pr.pr_reference f, latom - | TacArg(_,TacCall(loc,(f,l))) -> + | TacArg { CAst.v=TacCall {CAst.loc; v=(f,l)} } -> pr_with_comments ?loc (hov 1 ( pr.pr_reference f ++ spc () ++ prlist_with_sep spc pr_tacarg l)), lcall - | TacArg (_,a) -> + | TacArg { CAst.v=a } -> pr_tacarg a, latom - | TacML (loc,(s,l)) -> + | TacML { CAst.loc; v=(s,l) } -> pr_with_comments ?loc (pr.pr_extend 1 s l), lcall - | TacAlias (loc,(kn,l)) -> + | TacAlias { CAst.loc; v=(kn,l) } -> pr_with_comments ?loc (pr.pr_alias (level_of inherited) kn l), latom ) in @@ -1087,7 +1082,7 @@ let pr_goal_selector ~toplevel s = | TacNumgoals -> keyword "numgoals" | (TacCall _|Tacexp _ | TacGeneric _) as a -> - hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.tag a)))) + hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (CAst.make a)))) in pr_tac @@ -1179,7 +1174,7 @@ let pr_goal_selector ~toplevel s = pr_constant = pr_evaluable_reference_env env; pr_reference = pr_located pr_ltac_constant; pr_name = pr_id; - (** Those are not used by the atomic printer *) + (* Those are not used by the atomic printer *) pr_generic = (fun _ -> assert false); pr_extend = (fun _ _ _ -> assert false); pr_alias = (fun _ _ _ -> assert false); |