New Arguments vernacular

The new vernacular "Arguments" attaches to constants the extra-logical
piece of information regarding implicit arguments, notation scopes and
the behaviour of the simpl tactic. The About vernacular is extended to
print the new extra logical data for simpl.

Examples:

Arguments foo {A B}%type f [T] x.
  (* declares A B and T as implicit arguments, A B maximally inserted.
     declares type_scope on A and B *)

Arguments foo {A%type b%nat} p%myscope q.
  (* declares A and b as maximally inserted implicit arguments.
     declares type_scope on A, nat_scope on b and the scope delimited by
     myscope on p *)

Arguments foo (A B)%type c d.
  (* declares A and b in type_scope, but not as implicit arguments. *)

Arguments foo A B c.
  (* leaves implicit arguments and scopes declared for foo untouched *)

Arguments foo A B c : clear implicits
  (* equivalente too Implicit Arguments foo [] *)

Arguments foo A B c : clear scopes
  (* equivalente too Arguments Scope foo [_ _ _] *)

Arguments foo A B c : clear scopes, clear implicits
Arguments foo A B c : clear implicits, clear scopes
Arguments foo A B c : clear scopes and implicits
Arguments foo A B c : clear implicits and scopes
  (* equivalente too Arguments Scope foo [_ _ _]. Implcit Arguments foo [] *)

Arguments foo A B c : default implicits.
  (* equivalent to Implicit Arguments foo. *)

Arguments foo {A B} x , A [B] x.
  (* equivalent to Implicit Arguments foo [[A] [B]] [B]. *)

Arguments foo a !b c !d.
  (* foo is unfolded by simpl if b and d evaluate to a constructor *)

Arguments foo a b c / d.
  (* foo is unfolded by simpl if applied to 3 arguments *)

Arguments foo a !b c / d.
  (* foo is unfolded by simpl if applied to 3 arguments and if b
     evaluates to a constructor *)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14717 85f007b7-540e-0410-9357-904b9bb8a0f7

11 files changed, 336 insertions, 9 deletions

diff --git a/interp/notation.mli b/interp/notation.mli
index 52a7c2b99c..f92ef94ed3 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -48,6 +48,8 @@ val open_close_scope :
 val empty_scope_stack : scopes
 val push_scope : scope_name -> scopes -> scopes
 
+val find_scope : scope_name -> scope
+
 (** Declare delimiters for printing *)
 
 val declare_delimiters : scope_name -> delimiters -> unit
diff --git a/library/impargs.ml b/library/impargs.ml
index 2d5ffe9ab0..5d689faa0b 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -246,6 +246,10 @@ let compute_auto_implicits env flags enriching t =
   if enriching then compute_implicits_flags env flags true t
   else compute_implicits_gen false false false true true env t
 
+let compute_implicits_names env t =
+  let _, impls = compute_implicits_gen false false false false true env t in
+  List.map fst impls
+
 (* Extra information about implicit arguments *)
 
 type maximal_insertion = bool (* true = maximal contextual insertion *)
diff --git a/library/impargs.mli b/library/impargs.mli
index 6315745911..04251f332e 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -95,6 +95,8 @@ type manual_implicits = manual_explicitation list
 val compute_implicits_with_manual : env -> types -> bool ->
   manual_implicits -> implicit_status list
 
+val compute_implicits_names : env -> types -> name list
+
 (** {6 Computation of implicits (done using the global environment). } *)
 
 val declare_var_implicits : variable -> unit
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 78e01afd94..422da85447 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -581,10 +581,59 @@ GEXTEND Gram
 
       | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is
 
+      (* Arguments *)
+      | IDENT "Arguments"; qid = smart_global; 
+        impl = LIST1 [ l = LIST0
+        [ item = argument_spec ->
+            let id, r, s = item in [`Id (id,r,s,false,false)]
+        | "/" -> [`Slash]
+        | "("; items = LIST1 argument_spec; ")"; sc = OPT scope ->
+            let f x = match sc, x with
+            | None, x -> x | x, None -> Option.map (fun y -> loc, y) x
+            | Some _, Some _ -> error "scope declared twice" in
+            List.map (fun (id,r,s) -> `Id(id,r,f s,false,false)) items
+        | "["; items = LIST1 argument_spec; "]"; sc = OPT scope ->
+            let f x = match sc, x with
+            | None, x -> x | x, None -> Option.map (fun y -> loc, y) x
+            | Some _, Some _ -> error "scope declared twice" in
+            List.map (fun (id,r,s) -> `Id(id,r,f s,true,false)) items
+        | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope ->
+            let f x = match sc, x with
+            | None, x -> x | x, None -> Option.map (fun y -> loc, y) x
+            | Some _, Some _ -> error "scope declared twice" in
+            List.map (fun (id,r,s) -> `Id(id,r,f s,true,true)) items
+        ] -> l ] SEP ",";
+        mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] ->
+         let mods = match mods with None -> [] | Some l -> List.flatten l in
+         let impl = List.map List.flatten impl in
+         let rec aux n (narg, impl) = function
+           | `Id x :: tl -> aux (n+1) (narg, impl@[x]) tl
+           | `Slash :: tl -> aux (n+1) (n, impl) tl
+           | [] -> narg, impl in
+         let nargs, impl = List.split (List.map (aux 0 (-1, [])) impl) in
+         let nargs, rest = List.hd nargs, List.tl nargs in
+         if List.exists ((<>) nargs) rest then
+           error "All arguments lists must have the same length";
+         let err_incompat x y =
+           error ("Options \""^x^"\" and \""^y^"\" are incompatible") in
+         if nargs > 0 && List.mem `SimplNeverUnfold mods then
+           err_incompat "simpl never" "/";
+         if List.mem `SimplNeverUnfold mods &&
+            List.mem `SimplDontExposeCase mods then
+           err_incompat "simpl never" "simpl nomatch";
+         VernacArguments (use_section_locality(), qid, impl, nargs, 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 ]; "]" ->
+         warning "Arguments Scope is deprecated; use Arguments instead";
+	 VernacArgumentsScope (use_section_locality (),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 ] ->
+	   warning "Implicit Arguments is deprecated; use Arguments instead";
 	   VernacDeclareImplicits (use_section_locality (),qid,pos)
 
       | IDENT "Implicit"; "Type"; bl = reserv_list ->
@@ -601,12 +650,32 @@ GEXTEND Gram
 		  idl = LIST1 identref -> Some idl ] ->
 	     VernacGeneralizable (use_non_locality (), gen) ] ]
   ;
+  arguments_modifier:
+    [ [ IDENT "simpl"; IDENT "nomatch" -> [`SimplDontExposeCase]
+      | IDENT "simpl"; IDENT "never" -> [`SimplNeverUnfold]
+      | IDENT "default"; IDENT "implicits" -> [`DefaultImplicits]
+      | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits]
+      | IDENT "clear"; IDENT "scopes" -> [`ClearScopes]
+      | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" ->
+          [`ClearImplicits; `ClearScopes]
+      | IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" ->
+          [`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 ] ]
+  ;
+  argument_spec: [
+       [ b = OPT "!"; id = name ; s = OPT scope ->
+       snd id, b <> None, Option.map (fun x -> loc, x) s
+    ]
+  ];
   strategy_level:
     [ [ IDENT "expand" -> Conv_oracle.Expand
       | IDENT "opaque" -> Conv_oracle.Opaque
@@ -901,10 +970,6 @@ GEXTEND Gram
      | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
        refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
 
-     | IDENT "Arguments"; IDENT "Scope"; qid = smart_global;
-       "["; scl = LIST0 opt_scope; "]" ->
-	 VernacArgumentsScope (use_section_locality (),qid,scl)
-
      | IDENT "Infix"; local = obsolete_locality;
 	 op = ne_lstring; ":="; p = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
@@ -970,9 +1035,6 @@ GEXTEND Gram
       | IDENT "closed"; IDENT "binder" -> ETBinder false
     ] ]
   ;
-  opt_scope:
-    [ [ "_" -> None | sc = IDENT -> Some sc ] ]
-  ;
   production_item:
     [ [ s = ne_string -> TacTerm s
       | nt = IDENT;
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 6254d345f7..4e73b37939 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -835,6 +835,31 @@ let rec pr_vernac = function
 	prlist_with_sep spc (fun imps ->
 	  str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
 	  impls)
+  | VernacArguments (local, q, impl, nargs, mods) ->
+      hov 2 (pr_section_locality local ++ str"Arguments" ++ spc() ++
+        pr_smart_global q ++
+      let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in
+      let pr_if b x = if b then x else str "" in
+      let pr_br imp max x = match imp, max with
+        | true, false -> str "[" ++ x ++ str "]"
+        | true, true -> str "{" ++ x ++ str "}"
+        | _ -> x in
+      let rec aux n l =
+        match n, l with
+        | 0, l -> spc () ++ str"/" ++ aux ~-1 l
+        | _, [] -> mt()
+        | n, (id,k,s,imp,max) :: tl ->
+            spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++
+            aux (n-1) tl in
+      prlist_with_sep (fun () -> str", ") (aux nargs) impl ++
+      if mods <> [] then str" : " else str"" ++
+      prlist_with_sep (fun () -> str", " ++ spc()) (function
+        | `SimplDontExposeCase -> str "simpl nomatch"
+        | `SimplNeverUnfold -> str "simpl never"
+        | `DefaultImplicits -> str "default implicits"
+        | `ClearImplicits -> str "clear implicits"
+        | `ClearScopes -> str "clear scopes")
+        mods)
   | VernacReserve bl ->
       let n = List.length (List.flatten (List.map fst bl)) in
       hov 2 (str"Implicit Type" ++
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 06d148ec60..741f9201e8 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -151,6 +151,45 @@ let print_argument_scopes prefix = function
       str "]")]
   | _  -> []
 
+(*****************************)
+(** Printing simpl behaviour *)
+
+let print_simpl_behaviour ref =
+  match Tacred.get_simpl_behaviour ref with
+  | None -> []
+  | Some (recargs, nargs, flags) ->
+     let never = List.mem `SimplNeverUnfold flags in
+     let nomatch = List.mem `SimplDontExposeCase flags in
+     let pp_nomatch = spc() ++ if nomatch then
+       str "avoiding to expose match constructs" else str"" in
+     let pp_recargs = spc() ++ str "when the " ++
+       let rec aux = function
+         | [] -> mt()
+         | [x] -> str (ordinal (x+1))
+         | [x;y] -> str (ordinal (x+1)) ++ str " and " ++ str (ordinal (y+1))
+         | x::tl -> str (ordinal (x+1)) ++ str ", " ++ aux tl in
+       aux recargs ++ str (plural (List.length recargs) " argument") ++
+       str (plural (if List.length recargs >= 2 then 1 else 2) " evaluate") ++
+       str " to a constructor" in
+     let pp_nargs =
+       spc() ++ str "when applied to " ++ int nargs ++
+       str (plural nargs " argument") in
+     [hov 2 (str "The simpl tactic " ++
+     match recargs, nargs, never with
+     | _,_, true -> str "never unfolds " ++ pr_global ref
+     | [], 0, _ -> str "always unfolds " ++ pr_global ref
+     | _::_, n, _ when n < 0 ->
+        str "unfolds " ++ pr_global ref ++ pp_recargs ++ pp_nomatch
+     | _::_, n, _ when n > List.fold_left max 0 recargs ->
+        str "unfolds " ++ pr_global ref ++ pp_recargs ++
+        str " and" ++ pp_nargs ++ pp_nomatch
+     | _::_, _, _ ->
+        str "unfolds " ++ pr_global ref ++ pp_recargs ++ pp_nomatch
+     | [], n, _ when n > 0 ->
+        str "unfolds " ++ pr_global ref ++ pp_nargs ++ pp_nomatch
+     | _ -> str "unfolds " ++ pr_global ref ++ pp_nomatch )]
+;;
+
 (*********************)
 (** Printing Opacity *)
 
@@ -625,6 +664,7 @@ let print_about_any k =
       pr_infos_list
        ([print_ref false ref; blankline] @
 	print_name_infos ref @
+	print_simpl_behaviour ref @
 	print_opacity ref @
 	[hov 0 (str "Expands to: " ++ pr_located_qualid k)])
   | Syntactic kn ->
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
new file mode 100644
index 0000000000..139f9e9922
--- /dev/null
+++ b/test-suite/output/Arguments.out
@@ -0,0 +1,93 @@
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus avoiding to expose match constructs
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus when applied to 1 argument
+  avoiding to expose match constructs
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus
+  when the 1st argument evaluates to a constructor and
+  when applied to 1 argument avoiding to expose match constructs
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus
+  when the 1st and 2nd arguments evaluate to a constructor and
+  when applied to 2 arguments 
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus
+  when the 1st and 2nd arguments evaluate to a constructor 
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+pf :
+forall D1 C1 : Type,
+(D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
+
+Arguments D2, C2 are implicit
+Arguments D1, C1 are implicit and maximally inserted
+Argument scopes are [foo_scope type_scope _ _ _ _ _]
+The simpl tactic never unfolds pf
+pf is transparent
+Expands to: Constant Top.pf
+fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
+
+Arguments A, B, C are implicit and maximally inserted
+Argument scopes are [type_scope type_scope type_scope _ _ _]
+The simpl tactic unfolds fcomp when applied to 6 arguments 
+fcomp is transparent
+Expands to: Constant Top.fcomp
+volatile : nat -> nat
+
+Argument scope is [nat_scope]
+The simpl tactic always unfolds volatile
+volatile is transparent
+Expands to: Constant Top.volatile
+f : T1 -> T2 -> nat -> unit -> nat -> nat
+
+Argument scopes are [_ _ nat_scope _ nat_scope]
+f is transparent
+Expands to: Constant Top.S1.S2.f
+f : T1 -> T2 -> nat -> unit -> nat -> nat
+
+Argument scopes are [_ _ nat_scope _ nat_scope]
+The simpl tactic unfolds f
+  when the 3rd, 4th and 5th arguments evaluate to a constructor 
+f is transparent
+Expands to: Constant Top.S1.S2.f
+f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
+
+Argument T2 is implicit
+Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
+The simpl tactic unfolds f
+  when the 4th, 5th and 6th arguments evaluate to a constructor 
+f is transparent
+Expands to: Constant Top.S1.f
+f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
+
+Arguments T1, T2 are implicit
+Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
+The simpl tactic unfolds f
+  when the 5th, 6th and 7th arguments evaluate to a constructor 
+f is transparent
+Expands to: Constant Top.f
+f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
+
+The simpl tactic unfolds f
+  when the 5th, 6th and 7th arguments evaluate to a constructor 
+f is transparent
+Expands to: Constant Top.f
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
new file mode 100644
index 0000000000..c93d2505da
--- /dev/null
+++ b/test-suite/output/Arguments.v
@@ -0,0 +1,40 @@
+Arguments minus n m : simpl nomatch. 
+About minus.
+Arguments minus n / m : simpl nomatch. 
+About minus.
+Arguments minus !n / m : simpl nomatch. 
+About minus.
+Arguments minus !n !m /.
+About minus.
+Arguments minus !n !m.
+About minus.
+Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := 
+  fun x => (f (fst x), g (snd x)).
+Delimit Scope foo_scope with F.
+Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never.
+About pf.
+Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
+Arguments fcomp {A B C}%type_scope f g x /.
+About fcomp.
+Definition volatile := fun x : nat => x.
+Arguments volatile /.
+About volatile.
+Set Implicit Arguments.
+Section S1.
+Variable T1 : Type.
+Section S2.
+Variable T2 : Type.
+Fixpoint f (x : T1) (y : T2) n (v : unit) m {struct n} : nat :=
+  match n, m with
+  | 0,_ => 0
+  | S _, 0 => n
+  | S n', S m' => f x y n' v m' end.
+About f.
+Global Arguments f x y !n !v !m.
+About f.
+End S2.
+About f.
+End S1.
+About f.
+Arguments f : clear implicits and scopes.
+About f.
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 102c92237d..60b89c2236 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -165,6 +165,7 @@ let rec attribute_of_vernac_command = function
   | VernacHints _ -> []
   | VernacSyntacticDefinition _ -> []
   | VernacDeclareImplicits _ -> []
+  | VernacArguments _ -> [] 
   | VernacDeclareReduction _ -> []
   | VernacReserve _ -> []
   | VernacGeneralizable _ -> []
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 88b78a633f..71bd311890 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -763,6 +763,59 @@ let vernac_declare_implicits local r = function
       Impargs.declare_manual_implicits local (smart_global r) ~enriching:false
 	(List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps)
 
+let vernac_declare_arguments local r l nargs flags =
+  let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in
+  let names, rest = List.hd names, List.tl names in
+  if List.exists ((<>) names) rest then
+    error "All arguments lists must declare the same names";
+  let inf_names =
+    Impargs.compute_implicits_names (Global.env())
+      (Global.type_of_global (smart_global r)) in
+  let string_of_name = function Anonymous -> "_" | Name id -> string_of_id id in
+  let rec check ld li = match ld, li with
+    | [], [] -> ()
+    | [], l -> error ("The following arguments are not declared: " ^
+       (String.concat ", " (List.map string_of_name l)))
+    | x::_, [] -> error ("Extra argument " ^ string_of_name x)
+    | Name x::_, Name y::_ when x <> y -> error ("The declared name " ^
+        string_of_id x ^ " and the inferred one " ^ string_of_id y ^
+        " are different")
+    | _::ld, _::li -> check ld li in
+  if names <> [] then check names inf_names;
+  let implicits = List.map (Util.list_map_filter (function
+    | (Anonymous, _,_,_,_) | (_,_,_, false, _) -> None
+    | (Name id, _,_, true, max) -> Some (ExplByName id,max,false))) l in
+  (* All other infos are in the first item of l *)
+  let l = List.hd l in
+  let some_implicits_specified = implicits <> [[]] in
+  let scopes = List.map (function
+    | (_,_, None,_,_) -> None
+    | (_,_, Some (o, k), _,_) -> 
+        try Some(ignore(Notation.find_scope k); k)
+        with _ -> Some (Notation.find_delimiters_scope o k)) l in
+  let some_scopes_specified = List.exists ((<>) None) scopes in
+  let rargs =
+    Util.list_map_filter (function (n, true) -> Some n | _ -> None)
+      (Util.list_map_i (fun i (_, b, _,_,_) -> i, b) 0 l) in
+  if some_scopes_specified || List.mem `ClearScopes flags then
+    vernac_arguments_scope local r scopes;
+  if not some_implicits_specified && List.mem `DefaultImplicits flags then
+    vernac_declare_implicits local r []
+  else if some_implicits_specified || List.mem `ClearImplicits flags then
+    vernac_declare_implicits local r implicits;
+  if nargs >= 0 && nargs < List.fold_left max 0 rargs then
+    error "The \"/\" option must be places after the last \"!\"";
+  let rec narrow = function
+    | #Tacred.simpl_flag as x :: tl -> x :: narrow tl
+    | [] -> [] | _ :: tl -> narrow tl in
+  let flags = narrow flags in
+  if rargs <> [] || nargs >= 0 || flags <> [] then
+    match smart_global r with
+    | ConstRef _ as c ->
+       Tacred.set_simpl_behaviour local c (rargs, nargs, flags)
+    | _ -> error "Simpl behaviour can be declared for constants only"
+;;
+
 let vernac_reserve bl =
   let sb_decl = (fun (idl,c) ->
     let t = Constrintern.interp_type Evd.empty (Global.env()) c in
@@ -1377,6 +1430,7 @@ let interp c = match c with
   | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
   | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
   | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
+  | VernacArguments (local, qid, l, narg, flags) -> vernac_declare_arguments local qid l narg flags 
   | VernacReserve bl -> vernac_reserve bl
   | VernacGeneralizable (local,gen) -> vernac_generalizable local gen
   | VernacSetOpacity (local,qidl) -> vernac_set_opacity local qidl
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index bae6cfcdd9..575735230d 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -224,8 +224,6 @@ type vernac_expr =
   | VernacOpenCloseScope of (locality_flag * bool * scope_name)
   | VernacDelimiters of scope_name * string
   | VernacBindScope of scope_name * class_rawexpr list
-  | VernacArgumentsScope of locality_flag * reference or_by_notation *
-      scope_name option list
   | VernacInfix of locality_flag * (lstring * syntax_modifier list) *
       constr_expr * scope_name option
   | VernacNotation of
@@ -318,6 +316,12 @@ type vernac_expr =
       locality_flag * onlyparsing_flag
   | VernacDeclareImplicits of locality_flag * reference or_by_notation *
       (explicitation * bool * bool) list list
+  | VernacArguments of locality_flag * reference or_by_notation * 
+      ((name * bool * (loc * string) option * bool * bool) list) list *
+      int * [ `SimplDontExposeCase | `SimplNeverUnfold
+            | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list
+  | VernacArgumentsScope of locality_flag * reference or_by_notation *
+      scope_name option list
   | VernacReserve of simple_binder list
   | VernacGeneralizable of locality_flag * (lident list) option
   | VernacSetOpacity of