diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 37 |
1 files changed, 0 insertions, 37 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 8180e4503..7eb8396ac 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -155,13 +155,6 @@ open Decl_kinds let pr_locality local = if local then keyword "Local" else keyword "Global" - let pr_explanation (e,b,f) = - let a = match e with - | ExplByPos (n,_) -> anomaly (Pp.str "No more supported.") - | ExplByName id -> pr_id id in - let a = if f then str"!" ++ a else a in - if b then str "[" ++ a ++ str "]" else a - let pr_option_ref_value = function | QualidRefValue id -> pr_reference id | StringRefValue s -> qs s @@ -181,8 +174,6 @@ open Decl_kinds | BoolValue b -> mt() in pr_printoption a None ++ pr_opt_value b - let pr_topcmd _ = str"(* <Warning> : No printer for toplevel commands *)" - let pr_opt_hintbases l = match l with | [] -> mt() | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z @@ -593,8 +584,6 @@ open Decl_kinds ) | VernacUndoTo i -> return (keyword "Undo" ++ spc() ++ keyword "To" ++ pr_intarg i) - | VernacBacktrack (i,j,k) -> - return (keyword "Backtrack" ++ spc() ++ prlist_with_sep sep int [i;j;k]) | VernacFocus i -> return (keyword "Focus" ++ pr_opt int i) | VernacShow s -> @@ -655,16 +644,6 @@ open Decl_kinds keyword "Bind Scope" ++ spc () ++ str sc ++ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_class_rawexpr cll ) - | VernacArgumentsScope (q,scl) -> - let pr_opt_scope = function - | None -> str"_" - | Some sc -> str sc - in - return ( - keyword "Arguments Scope" - ++ spc() ++ pr_smart_global q - ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" - ) | VernacInfix (({v=s},mv),q,sn) -> (* A Verifier *) return ( hov 0 (hov 0 (keyword "Infix " @@ -1019,18 +998,6 @@ open Decl_kinds | Some Flags.Current -> [SetOnlyParsing] | Some v -> [SetCompatVersion v])) ) - | VernacDeclareImplicits (q,[]) -> - return ( - hov 2 (keyword "Implicit Arguments" ++ spc() ++ pr_smart_global q) - ) - | VernacDeclareImplicits (q,impls) -> - return ( - hov 1 (keyword "Implicit Arguments" ++ spc () ++ - spc() ++ pr_smart_global q ++ spc() ++ - prlist_with_sep spc (fun imps -> - str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") - impls) - ) | VernacArguments (q, args, more_implicits, nargs, mods) -> return ( hov 2 ( @@ -1189,10 +1156,6 @@ open Decl_kinds ++ prlist_with_sep sep (pr_comment pr_constr) l) ) - (* Toplevel control *) - | VernacToplevelControl exn -> - return (pr_topcmd exn) - (* For extension *) | VernacExtend (s,c) -> return (pr_extend s c) |