diff options
| author |  Jasper Hugunin <jasperh@cs.washington.edu> | 2018-02-22 20:08:52 -0800 |
|---|---|---|
| committer | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-03-30 17:48:17 -0700 |
| commit | ef6202218c92bf3fb5bcdeca0c372e5d124cd537 (patch) | |
| tree | 0088016d1a47d56c3f8c1825144e3ccba01aaccd /printing | |
| parent | 0fa8b8cb53050d48187fd2577f2fef0f1a45d024 (diff) | |
Remove deprecated commands Arguments Scope and Implicit Arguments
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 7df0a0c94..2706893ac 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 @@ -653,16 +646,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 " @@ -1016,18 +999,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 ( |