Remove deprecated commands Arguments Scope and Implicit Arguments

Author: jashug

intf/vernacexpr.ml

@@ -409,17 +409,13 @@ type nonrec vernac_expr =
   | VernacHints of string list * hints_expr
   | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) *
       onlyparsing_flag
-  | VernacDeclareImplicits of reference or_by_notation *
-      (explicitation * bool * bool) list list
   | VernacArguments of reference or_by_notation *
       vernac_argument_status list (* Main arguments status list *) *
         (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) *
       int option (* Number of args to trigger reduction *) *
         [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
           `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
           `DefaultImplicits ] list
-  | VernacArgumentsScope of reference or_by_notation *
-      scope_name option list
   | VernacReserve of simple_binder list
   | VernacGeneralizable of (lident list) option
   | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list)

parsing/g_vernac.ml4

@@ -601,14 +601,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;
@@ -691,20 +683,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
 
@@ -734,12 +712,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 ] ]
   ;

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 (

stm/vernac_classifier.ml

@@ -145,7 +145,7 @@ let classify_vernac e =
     | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
     | VernacChdir _ 
     | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
-    | VernacDeclareImplicits _ | VernacArguments _ | VernacArgumentsScope _
+    | VernacArguments _
     | VernacReserve _
     | VernacGeneralizable _
     | VernacSetOpacity _ | VernacSetStrategy _

tools/gallina-syntax.el

@@ -432,7 +432,6 @@
      ("Add Semi Ring" nil "Add Semi Ring #." t "Add\\s-+Semi\\s-+Ring")
      ("Add Setoid" nil "Add Setoid #." t "Add\\s-+Setoid")
      ("Admit Obligations" "oblsadmit" "Admit Obligations." nil "Admit\\s-+Obligations")
-     ("Arguments Scope" "argsc" "Arguments Scope @{id} [ @{_} ]" t "Arguments\\s-+Scope")
      ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope")
      ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure")
      ("Cd" nil "Cd #." nil "Cd")

vernac/vernacentries.ml

@@ -2025,7 +2025,6 @@ let interp ?proof ~atts ~st c =
   | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
   | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
   | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s)
-  | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope ~atts qid scl
   | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc
   | VernacNotation (c,infpl,sc) ->
       vernac_notation ~atts c infpl sc
@@ -2099,8 +2098,6 @@ let interp ?proof ~atts ~st c =
       vernac_hints ~atts dbnames hints
   | VernacSyntacticDefinition (id,c,b) ->
       vernac_syntactic_definition ~atts id c b
-  | VernacDeclareImplicits (qid,l) ->
-      vernac_declare_implicits ~atts qid l
   | VernacArguments (qid, args, more_implicits, nargs, flags) ->
       vernac_arguments ~atts qid args more_implicits nargs flags
   | VernacReserve bl -> vernac_reserve bl
@@ -2168,7 +2165,7 @@ let check_vernac_supports_locality c l =
     | VernacDeclareMLModule _
     | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
     | VernacSyntacticDefinition _
-    | VernacArgumentsScope _ | VernacDeclareImplicits _ | VernacArguments _
+    | VernacArguments _
     | VernacGeneralizable _
     | VernacSetOpacity _ | VernacSetStrategy _
     | VernacSetOption _ | VernacUnsetOption _