diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 34 |
1 files changed, 0 insertions, 34 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b947253b71..593dcbf58c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -592,14 +592,6 @@ GEXTEND Gram ; END -let warn_deprecated_arguments_scope = - CWarnings.create ~name:"deprecated-arguments-scope" ~category:"deprecated" - (fun () -> strbrk "Arguments Scope is deprecated; use Arguments instead") - -let warn_deprecated_implicit_arguments = - CWarnings.create ~name:"deprecated-implicit-arguments" ~category:"deprecated" - (fun () -> strbrk "Implicit Arguments is deprecated; use Arguments instead") - (* Extensions: implicits, coercions, etc. *) GEXTEND Gram GLOBAL: gallina_ext instance_name hint_info; @@ -682,20 +674,6 @@ GEXTEND Gram let more_implicits = Option.default [] more_implicits in VernacArguments (qid, args, more_implicits, !slash_position, mods) - - (* moved there so that camlp5 factors it with the previous rule *) - | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; - "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" -> - warn_deprecated_arguments_scope ~loc:!@loc (); - VernacArgumentsScope (qid,scl) - - (* Implicit *) - | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; - pos = LIST0 [ "["; l = LIST0 implicit_name; "]" -> - List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> - warn_deprecated_implicit_arguments ~loc:!@loc (); - VernacDeclareImplicits (qid,pos) - | IDENT "Implicit"; "Type"; bl = reserv_list -> VernacReserve bl @@ -725,12 +703,6 @@ GEXTEND Gram [`ClearImplicits; `ClearScopes] ] ] ; - implicit_name: - [ [ "!"; id = ident -> (id, false, true) - | id = ident -> (id,false,false) - | "["; "!"; id = ident; "]" -> (id,true,true) - | "["; id = ident; "]" -> (id,true, false) ] ] - ; scope: [ [ "%"; key = IDENT -> key ] ] ; @@ -836,10 +808,6 @@ GEXTEND Gram | IDENT "Cd" -> VernacChdir None | IDENT "Cd"; dir = ne_string -> VernacChdir (Some dir) - (* Toplevel control *) - | IDENT "Drop" -> VernacToplevelControl Drop - | IDENT "Quit" -> VernacToplevelControl Quit - | IDENT "Load"; verbosely = [ IDENT "Verbose" -> true | -> false ]; s = [ s = ne_string -> s | s = IDENT -> s ] -> VernacLoad (verbosely, s) @@ -1060,8 +1028,6 @@ GEXTEND Gram | IDENT "Back" -> VernacBack 1 | IDENT "Back"; n = natural -> VernacBack n | IDENT "BackTo"; n = natural -> VernacBackTo n - | IDENT "Backtrack"; n = natural ; m = natural ; p = natural -> - VernacBacktrack (n,m,p) (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> |