Imported Upstream version 8.8.2upstream/8.8.2

9 files changed, 169 insertions, 336 deletions

diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp
index d0ab5d80..9c25dcfa 100644
--- a/grammar/argextend.mlp
+++ b/grammar/argextend.mlp
@@ -1,16 +1,25 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Q_util
-open GramCompat
 
-let loc = CompatLoc.ghost
-let default_loc = <:expr< Loc.ghost >>
+let loc = Ploc.dummy
+
+IFDEF STRICT THEN
+  let ploc_vala x = Ploc.VaVal x
+ELSE
+  let ploc_vala x = x
+END
+
+let declare_str_items loc l =
+  MLast.StDcl (loc, ploc_vala l) (* correspond to <:str_item< declare $list:l'$ end >> *)
 
 let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >>
 
@@ -32,7 +41,8 @@ let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>
 let make_act loc act pil =
   let rec make = function
     | [] -> <:expr< (fun loc -> $act$) >>
-    | ExtNonTerminal (_, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >>
+    | ExtNonTerminal (_, None) :: tl -> <:expr< (fun $lid:"_"$ -> $make tl$) >>
+    | ExtNonTerminal (_, Some p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >>
     | ExtTerminal _ :: tl ->
 	<:expr< (fun _ -> $make tl$) >> in
   make (List.rev pil)
@@ -55,7 +65,7 @@ let is_ident x = function
 | _ -> false
 
 let make_extend loc s cl wit = match cl with
-| [[ExtNonTerminal (Uentry e, id)], act] when is_ident id act ->
+| [[ExtNonTerminal (Uentry e, Some id)], act] when is_ident id act ->
   (** Special handling of identity arguments by not redeclaring an entry *)
   <:str_item<
     value $lid:s$ =
@@ -129,11 +139,11 @@ let declare_tactic_argument loc s (typ, f, g, h) cl =
       let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in
       <:expr<
         let f = $lid:f$ in
-        fun ist v -> Ftactic.nf_s_enter { Proofview.Goal.s_enter = fun gl ->
+        fun ist v -> Ftactic.enter (fun gl ->
           let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in
           let v = Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v in
-          Sigma.Unsafe.of_pair (Ftactic.return v, sigma)
-        }
+          Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Ftactic.return v)
+        )
       >> in
   let subst = match h with
     | None ->
@@ -170,22 +180,16 @@ let declare_vernac_argument loc s pr cl =
   let se = mlexpr_of_string s in
   let wit = <:expr< $lid:"wit_"^s$ >> in
   let pr_rules = match pr with
-    | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >>
+    | None -> <:expr< fun _ _ _ _ -> Pp.str $str:"[No printer for "^s^"]"$ >>
     | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in
   declare_str_items loc
    [ <:str_item<
       value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) =
         Genarg.create_arg $se$ >>;
      make_extend loc s cl wit;
-    <:str_item< do {
-      Pptactic.declare_extra_genarg_pprule $wit$
-        $pr_rules$
-        (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not globwit printer"))
-        (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not wit printer")) }
-      >> ]
+    <:str_item< Pptactic.declare_extra_vernac_genarg_pprule $wit$ $pr_rules$ >> ]
 
 open Pcaml
-open PcamlSig (* necessary for camlp4 *)
 
 EXTEND
   GLOBAL: str_item;
@@ -239,10 +243,13 @@ EXTEND
   genarg:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let e = parse_user_entry e "" in
-        ExtNonTerminal (e, s)
+        ExtNonTerminal (e, Some s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let e = parse_user_entry e sep in
-        ExtNonTerminal (e, s)
+        ExtNonTerminal (e, Some s)
+      | e = LIDENT ->
+        let e = parse_user_entry e "" in
+        ExtNonTerminal (e, None)
       | s = STRING -> ExtTerminal s
     ] ]
   ;
diff --git a/grammar/compat5.ml b/grammar/compat5.ml
deleted file mode 100644
index 33c1cd60..00000000
--- a/grammar/compat5.ml
+++ /dev/null
@@ -1,13 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* This file is meant for camlp5, for which there is nothing to
-   add to gain camlp5 compatibility :-).
-
-   See [compat5.mlp] for the [camlp4] counterpart
-*)
diff --git a/grammar/compat5.mlp b/grammar/compat5.mlp
deleted file mode 100644
index 8473a1fb..00000000
--- a/grammar/compat5.mlp
+++ /dev/null
@@ -1,23 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Adding a bit of camlp5 syntax to camlp4 for compatibility:
-    - GEXTEND ... becomes EXTEND ...
-*)
-
-open Camlp4.PreCast
-
-let rec my_token_filter = parser
-  | [< '(KEYWORD "GEXTEND", loc); s >] ->
-    [< '(KEYWORD "EXTEND", loc); my_token_filter s >]
-  | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >]
-  | [< >] -> [< >]
-
-let _ =
-  Token.Filter.define_filter (Gram.get_filter())
-    (fun prev strm -> prev (my_token_filter strm))
diff --git a/grammar/compat5b.mlp b/grammar/compat5b.mlp
deleted file mode 100644
index 46802a82..00000000
--- a/grammar/compat5b.mlp
+++ /dev/null
@@ -1,23 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Adding a bit of camlp5 syntax to camlp4 for compatibility:
-    - EXTEND ... becomes EXTEND Gram ...
-*)
-
-open Camlp4.PreCast
-
-let rec my_token_filter = parser
-  | [< '(KEYWORD "EXTEND",_ as t); s >] ->
-    [< 't; '(UIDENT "Gram", Loc.ghost); my_token_filter s >]
-  | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >]
-  | [< >] -> [< >]
-
-let _ =
-  Token.Filter.define_filter (Gram.get_filter())
-    (fun prev strm -> prev (my_token_filter strm))
diff --git a/grammar/gramCompat.mlp b/grammar/gramCompat.mlp
deleted file mode 100644
index 6246da7b..00000000
--- a/grammar/gramCompat.mlp
+++ /dev/null
@@ -1,86 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Compatibility file depending on ocaml/camlp4 version *)
-
-(** Misc module emulation *)
-
-IFDEF CAMLP5 THEN
-
-module CompatLoc = struct
-  include Ploc
-  let ghost = dummy
-  let merge = encl
-end
-
-ELSE
-
-module CompatLoc = Camlp4.PreCast.Loc
-
-END
-
-IFDEF CAMLP5 THEN
-
-module PcamlSig = struct end
-
-ELSE
-
-module PcamlSig = Camlp4.Sig
-module Ast = Camlp4.PreCast.Ast
-module Pcaml = Camlp4.PreCast.Syntax
-module MLast = Ast
-
-END
-
-(** Compatibility with camlp5 strict mode *)
-IFDEF CAMLP5 THEN
-  IFDEF STRICT THEN
-    let vala x = Ploc.VaVal x
-  ELSE
-    let vala x = x
-  END
-ELSE
-  let vala x = x
-END
-
-(** Fix a quotation difference in [str_item] *)
-
-let declare_str_items loc l =
-IFDEF CAMLP5 THEN
-  MLast.StDcl (loc, vala l) (* correspond to <:str_item< declare $list:l'$ end >> *)
-ELSE
-  Ast.stSem_of_list l
-END
-
-(** Quotation difference for match clauses *)
-
-let default_patt loc =
-  (<:patt< _ >>, vala None, <:expr< failwith "Extension: cannot occur" >>)
-
-IFDEF CAMLP5 THEN
-
-let make_fun loc cl =
-  let l = cl @ [default_patt loc] in
-  MLast.ExFun (loc, vala l)  (* correspond to <:expr< fun [ $list:l$ ] >> *)
-
-ELSE
-
-let make_fun loc cl =
-  let mk_when = function
-    | Some w -> w
-    | None -> Ast.ExNil loc
-  in
-  let mk_clause (patt,optwhen,expr) =
-    (* correspond to <:match_case< ... when ... -> ... >> *)
-    Ast.McArr (loc, patt, mk_when optwhen, expr) in
-  let init = mk_clause (default_patt loc) in
-  let add_clause x acc = Ast.McOr (loc, mk_clause x, acc) in
-  let l = List.fold_right add_clause cl init in
-  Ast.ExFun (loc,l) (* correspond to <:expr< fun [ $l$ ] >> *)
-
-END
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index a5e36e47..323a1235 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -1,13 +1,13 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open GramCompat (* necessary for camlp4 *)
-
 type argument_type =
 | ListArgType of argument_type
 | OptArgType of argument_type
@@ -25,7 +25,7 @@ type user_symbol =
 
 type extend_token =
 | ExtTerminal of string
-| ExtNonTerminal of user_symbol * string
+| ExtNonTerminal of user_symbol * string option
 
 val mlexpr_of_list :  ('a -> MLast.expr) -> 'a list -> MLast.expr
 
@@ -41,6 +41,8 @@ val mlexpr_of_string : string -> MLast.expr
 
 val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr
 
+val mlexpr_of_name : ('a -> MLast.expr) -> 'a option -> MLast.expr
+
 val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.expr
 
 val type_of_user_symbol : user_symbol -> argument_type
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 2d5c4089..6cdd2ec1 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -1,15 +1,15 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* This file defines standard combinators to build ml expressions *)
 
-open GramCompat
-
 type argument_type =
 | ListArgType of argument_type
 | OptArgType of argument_type
@@ -27,23 +27,23 @@ type user_symbol =
 
 type extend_token =
 | ExtTerminal of string
-| ExtNonTerminal of user_symbol * string
+| ExtNonTerminal of user_symbol * string option
 
 let mlexpr_of_list f l =
   List.fold_right
     (fun e1 e2 ->
       let e1 = f e1 in
-       let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
+       let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
        <:expr< [$e1$ :: $e2$] >>)
-    l (let loc = CompatLoc.ghost in <:expr< [] >>)
+    l (let loc = Ploc.dummy in <:expr< [] >>)
 
 let mlexpr_of_pair m1 m2 (a1,a2) =
   let e1 = m1 a1 and e2 = m2 a2 in
-  let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
+  let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
   <:expr< ($e1$, $e2$) >>
 
 (* We don't give location for tactic quotation! *)
-let loc = CompatLoc.ghost
+let loc = Ploc.dummy
 
 
 let mlexpr_of_bool = function
@@ -58,6 +58,10 @@ let mlexpr_of_option f = function
   | None -> <:expr< None >>
   | Some e -> <:expr< Some $f e$ >>
 
+let mlexpr_of_name f = function
+  | None -> <:expr< Names.Name.Anonymous >>
+  | Some e -> <:expr< Names.Name.Name $f e$ >>
+
 let symbol_of_string s = <:expr< Extend.Atoken (CLexer.terminal $str:s$) >>
 
 let rec mlexpr_of_prod_entry_key f = function
@@ -66,12 +70,12 @@ let rec mlexpr_of_prod_entry_key f = function
   | Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >>
   | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >>
   | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >>
-  | Uentry e -> <:expr< Extend.Aentry $f e$ >>
+  | Uentry e -> <:expr< Extend.Aentry ($f e$) >>
   | Uentryl (e, l) ->
     (** Keep in sync with Pcoq! *)
     assert (e = "tactic");
-    if l = 5 then <:expr< Extend.Aentry (Pcoq.Tactic.binder_tactic) >>
-    else <:expr< Extend.Aentryl (Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >>
+    if l = 5 then <:expr< Extend.Aentry Pltac.binder_tactic >>
+    else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_int l$ >>
 
 let rec type_of_user_symbol = function
 | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) ->
@@ -92,10 +96,14 @@ let coincide s pat off =
   done;
   !break
 
+let check_separator sep =
+  if sep <> "" then failwith "Separator is only for arguments with suffix _list_sep."
+
 let rec parse_user_entry s sep =
   let l = String.length s in
   if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
     let entry = parse_user_entry (String.sub s 3 (l-8)) "" in
+    check_separator sep;
     Ulist1 entry
   else if l > 12 && coincide s "ne_" 0 &&
                    coincide s "_list_sep" (l-9) then
@@ -103,16 +111,20 @@ let rec parse_user_entry s sep =
     Ulist1sep (entry, sep)
   else if l > 5 && coincide s "_list" (l-5) then
     let entry = parse_user_entry (String.sub s 0 (l-5)) "" in
+    check_separator sep;
     Ulist0 entry
   else if l > 9 && coincide s "_list_sep" (l-9) then
     let entry = parse_user_entry (String.sub s 0 (l-9)) "" in
     Ulist0sep (entry, sep)
   else if l > 4 && coincide s "_opt" (l-4) then
     let entry = parse_user_entry (String.sub s 0 (l-4)) "" in
+    check_separator sep;
     Uopt entry
   else if l = 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
     let n = Char.code s.[6] - 48 in
+    check_separator sep;
     Uentryl ("tactic", n)
   else
     let s = match s with "hyp" -> "var" | _ -> s in
+    check_separator sep;
     Uentry s
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 683a7e2f..525be643 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -1,18 +1,17 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Implementation of the TACTIC EXTEND macro. *)
 
 open Q_util
 open Argextend
-open GramCompat
-
-let dloc = <:expr< Loc.ghost >>
 
 let plugin_name = <:expr< __coq_plugin_name >>
 
@@ -21,142 +20,65 @@ let mlexpr_of_ident id =
   let id = "$" ^ id in
   <:expr< Names.Id.of_string_soft $str:id$ >>
 
-let rec make_patt = function
-  | [] -> <:patt< [] >>
-  | ExtNonTerminal (_, p) :: l ->
-      <:patt< [ $lid:p$ :: $make_patt l$ ] >>
-  | _::l -> make_patt l
-
-let rec make_let raw e = function
-  | [] -> <:expr< fun $lid:"ist"$ -> $e$ >>
-  | ExtNonTerminal (g, p) :: l ->
-      let t = type_of_user_symbol g in
-      let loc = MLast.loc_of_expr e in
-      let e = make_let raw e l in
-      let v =
-        if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >>
-               else <:expr< Tacinterp.Value.cast $make_topwit    loc t$ $lid:p$ >> in
-      <:expr< let $lid:p$ = $v$ in $e$ >>
-  | _::l -> make_let raw e l
-
-let make_clause (pt,_,e) =
-  (make_patt pt,
-   vala None,
-   make_let false e pt)
-
-let make_fun_clauses loc s l =
-  let map c = GramCompat.make_fun loc [make_clause c] in
-  mlexpr_of_list map l
-
-let get_argt e = <:expr< (fun e -> match e with [ Genarg.ExtraArg tag -> tag | _ -> assert False ]) $e$ >>
-
 let rec mlexpr_of_symbol = function
-| Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >>
-| Ulist1sep (s,sep) -> <:expr< Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >>
-| Ulist0 s -> <:expr< Extend.Ulist0 $mlexpr_of_symbol s$ >>
-| Ulist0sep (s,sep) -> <:expr< Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >>
-| Uopt s -> <:expr< Extend.Uopt $mlexpr_of_symbol s$ >>
+| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >>
+| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >>
+| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >>
 | Uentry e ->
-  let arg = get_argt <:expr< $lid:"wit_"^e$ >> in
-  <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >>
+  let wit = <:expr< $lid:"wit_"^e$ >> in
+  <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >>
 | Uentryl (e, l) ->
   assert (e = "tactic");
-  let arg = get_argt <:expr< Constrarg.wit_tactic >> in
-  <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>>
-
-let make_prod_item = function
-  | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >>
-  | ExtNonTerminal (g, id) ->
-    <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_ident id$ >>
-
-let mlexpr_of_clause cl =
-  mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl
-
-(** Special treatment of constr entries *)
-let is_constr_gram = function
-| ExtTerminal _ -> false
-| ExtNonTerminal (Uentry "constr", _) -> true
-| _ -> false
-
-let make_var = function
-  | ExtNonTerminal (_, p) -> Some p
-  | _ -> assert false
-
-let declare_tactic loc s c cl = match cl with
-| [(ExtTerminal name) :: rem, _, tac] when List.for_all is_constr_gram rem ->
-  (** The extension is only made of a name followed by constr entries: we do not
-      add any grammar nor printing rule and add it as a true Ltac definition. *)
-  let patt = make_patt rem in
-  let vars = List.map make_var rem in
-  let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in
-  let entry = mlexpr_of_string s in
-  let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
-  let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in
-  let name = mlexpr_of_string name in
-  let tac = match rem with
-  | [] ->
-    (** Special handling of tactics without arguments: such tactics do not do
-        a Proofview.Goal.nf_enter to compute their arguments. It matters for some
-        whole-prof tactics like [shelve_unifiable]. *)
-      <:expr< fun _ $lid:"ist"$ -> $tac$ >>
-  | _ ->
-      let f = GramCompat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
-      <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >>
-  in
-  (** Arguments are not passed directly to the ML tactic in the TacML node,
-      the ML tactic retrieves its arguments in the [ist] environment instead.
-      This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
-  let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML ($dloc$, $ml$, [])) >> in
-  let name = <:expr< Names.Id.of_string $name$ >> in
-  declare_str_items loc
-    [ <:str_item< do {
-      let obj () = Tacenv.register_ltac True False $name$ $body$ in
-      let () = Tacenv.register_ml_tactic $se$ [|$tac$|] in
-      Mltop.declare_cache_obj obj $plugin_name$ } >>
-    ]
-| _ ->
-  (** Otherwise we add parsing and printing rules to generate a call to a
-      TacML tactic. *)
-  let entry = mlexpr_of_string s in
-  let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
-  let gl = mlexpr_of_clause cl in
-  let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in
-  declare_str_items loc
-    [ <:str_item< do {
-        Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$);
-        Mltop.declare_cache_obj $obj$ $plugin_name$; } >>
-    ]
+  let wit = <:expr< $lid:"wit_"^e$ >> in
+  <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>>
+
+let rec mlexpr_of_clause = function
+| [] -> <:expr< TyNil >>
+| ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >>
+| ExtNonTerminal(g,None) :: cl ->
+  <:expr< TyAnonArg(Loc.tag($mlexpr_of_symbol g$), $mlexpr_of_clause cl$) >>
+| ExtNonTerminal(g,Some id) :: cl ->
+  <:expr< TyArg(Loc.tag($mlexpr_of_symbol g$, $mlexpr_of_ident id$), $mlexpr_of_clause cl$) >>
+
+let rec binders_of_clause e = function
+| [] -> <:expr< fun ist -> $e$ >>
+| ExtNonTerminal(_,None) :: cl -> binders_of_clause e cl
+| ExtNonTerminal(_,Some id) :: cl -> <:expr< fun $lid:id$ -> $binders_of_clause e cl$ >>
+| _ :: cl -> binders_of_clause e cl
 
 open Pcaml
-open PcamlSig (* necessary for camlp4 *)
 
 EXTEND
   GLOBAL: str_item;
   str_item:
     [ [ "TACTIC"; "EXTEND"; s = tac_name;
-        c = OPT [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> ];
+        level = OPT [ "AT"; UIDENT "LEVEL"; level = INT -> level ];
         OPT "|"; l = LIST1 tacrule SEP "|";
         "END" ->
-         declare_tactic loc s c l ] ]
+        let level = match level with Some i -> int_of_string i | None -> 0 in
+        let level = mlexpr_of_int level in
+        let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in
+        declare_str_items loc [ <:str_item< Tacentries.tactic_extend $plugin_name$ $str:s$ ~{ level = $level$ } $l$ >> ] ] ]
   ;
   tacrule:
     [ [ "["; l = LIST1 tacargs; "]";
-        c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> c ];
         "->"; "["; e = Pcaml.expr; "]" ->
-	(match l with
-	  | ExtNonTerminal _ :: _ ->
-	    (* En attendant la syntaxe de tacticielles *)
-	    failwith "Tactic syntax must start with an identifier"
-	  | _ -> (l,c,e))
+         <:expr< TyML($mlexpr_of_clause l$, $binders_of_clause e l$) >>
     ] ]
   ;
+
   tacargs:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let e = parse_user_entry e "" in
-        ExtNonTerminal (e, s)
+        ExtNonTerminal (e, Some s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let e = parse_user_entry e sep in
-        ExtNonTerminal (e, s)
+        ExtNonTerminal (e, Some s)
+      | e = LIDENT ->
+        let e = parse_user_entry e "" in
+        ExtNonTerminal (e, None)
       | s = STRING ->
 	let () = if s = "" then failwith "Empty terminal." in
         ExtTerminal s
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index 04b117fb..a2872d07 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -1,17 +1,17 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Implementation of the VERNAC EXTEND macro. *)
 
 open Q_util
 open Argextend
-open Tacextend
-open GramCompat
 
 type rule = {
   r_head : string option;
@@ -26,9 +26,24 @@ type rule = {
   (** Whether this entry is deprecated *)
 }
 
+(** Quotation difference for match clauses *)
+
+let default_patt loc =
+  (<:patt< _ >>, ploc_vala None, <:expr< failwith "Extension: cannot occur" >>)
+
+let make_fun loc cl =
+  let l = cl @ [default_patt loc] in
+  MLast.ExFun (loc, ploc_vala l)  (* correspond to <:expr< fun [ $list:l$ ] >> *)
+
+let rec make_patt = function
+  | [] -> <:patt< [] >>
+  | ExtNonTerminal (_, Some p) :: l ->
+      <:patt< [ $lid:p$ :: $make_patt l$ ] >>
+  | _::l -> make_patt l
+
 let rec make_let e = function
   | [] -> e
-  | ExtNonTerminal (g, p) :: l ->
+  | ExtNonTerminal (g, Some p) :: l ->
       let t = type_of_user_symbol g in
       let loc = MLast.loc_of_expr e in
       let e = make_let e l in
@@ -37,13 +52,13 @@ let rec make_let e = function
 
 let make_clause { r_patt = pt; r_branch = e; } =
   (make_patt pt,
-   vala None,
+   ploc_vala None,
    make_let e pt)
 
 (* To avoid warnings *)
 let mk_ignore c pt =
   let fold accu = function
-  | ExtNonTerminal (_, p) -> p :: accu
+  | ExtNonTerminal (_, Some p) -> p :: accu
   | _ -> accu
   in
   let names = List.fold_left fold [] pt in
@@ -55,12 +70,12 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
   match c ,cg with
   | Some c, _ ->
      (make_patt pt,
-      vala None,
+      ploc_vala None,
       make_let (mk_ignore c pt) pt)
   | None, Some cg ->
      (make_patt pt,
-      vala None,
-      <:expr< fun () -> $cg$ $str:s$ >>)
+      ploc_vala None,
+      <:expr< fun loc -> $cg$ $str:s$ >>)
   | None, None -> prerr_endline
       (("Vernac entry \""^s^"\" misses a classifier. "^
          "A classifier is a function that returns an expression "^
@@ -82,8 +97,8 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
        ("Specific classifiers have precedence over global "^
          "classifiers. Only one classifier is called.") ^ "\n");
     (make_patt pt,
-      vala None,
-      <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>)
+      ploc_vala None,
+      <:expr< fun () -> ( CErrors.anomaly (Pp.str "No classification given for command " ^ s ) ) >>)
 
 let make_fun_clauses loc s l =
   let map c =
@@ -91,22 +106,23 @@ let make_fun_clauses loc s l =
     | None -> false
     | Some () -> true
     in
-    let cl = GramCompat.make_fun loc [make_clause c] in
+    let cl = make_fun loc [make_clause c] in
     <:expr< ($mlexpr_of_bool depr$, $cl$)>>
   in
   mlexpr_of_list map l
 
 let make_fun_classifiers loc s c l =
-  let cl = List.map (fun x -> GramCompat.make_fun loc [make_clause_classifier c s x]) l in
+  let cl = List.map (fun x -> make_fun loc [make_clause_classifier c s x]) l in
   mlexpr_of_list (fun x -> x) cl
 
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
-  | ExtNonTerminal (g, id) ->
+  | ExtNonTerminal (g, ido) ->
     let nt = type_of_user_symbol g in
     let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in
-      <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
-      $mlexpr_of_prod_entry_key base g$ >>
+    let typ = match ido with None -> None | Some _ -> Some nt in
+      <:expr< Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ ,
+      $mlexpr_of_prod_entry_key base g$ ) ) >>
 
 let mlexpr_of_clause cl =
   let mkexpr { r_head = a; r_patt = b; } = match a with
@@ -128,7 +144,6 @@ let declare_command loc s c nt cl =
       } >> ]
 
 open Pcaml
-open PcamlSig (* necessary for camlp4 *)
 
 EXTEND
   GLOBAL: str_item;
@@ -137,6 +152,10 @@ EXTEND
         OPT "|"; l = LIST1 rule SEP "|";
         "END" ->
          declare_command loc s c <:expr<None>> l
+      | "VERNAC"; "COMMAND"; "FUNCTIONAL"; "EXTEND"; s = UIDENT; c = OPT classification;
+        OPT "|"; l = LIST1 fun_rule SEP "|";
+        "END" ->
+         declare_command loc s c <:expr<None>> l
       | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; c = OPT classification;
         OPT "|"; l = LIST1 rule SEP "|";
         "END" ->
@@ -144,7 +163,7 @@ EXTEND
       | "DECLARE"; "PLUGIN"; name = STRING ->
         declare_str_items loc [
           <:str_item< value __coq_plugin_name = $str:name$ >>;
-          <:str_item< value _ = Mltop.add_known_module $str:name$ >>;
+          <:str_item< value _ = Mltop.add_known_module __coq_plugin_name >>;
         ]
       ] ]
   ;
@@ -159,31 +178,47 @@ EXTEND
   deprecation:
     [ [ "DEPRECATED" -> () ] ]
   ;
-  (* spiwack: comment-by-guessing: it seems that the isolated string (which
-      otherwise could have been another argument) is not passed to the
-      VernacExtend interpreter function to discriminate between the clauses. *)
+  (* spiwack: comment-by-guessing: it seems that the isolated string
+      (which otherwise could have been another argument) is not passed
+      to the VernacExtend interpreter function to discriminate between
+      the clauses. *)
   rule:
     [ [ "["; s = STRING; l = LIST0 args; "]";
         d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
       let () = if s = "" then failwith "Command name is empty." in
-      let b = <:expr< fun () -> $e$ >> in
+      let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in
+      { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
+      | "[" ; "-" ; l = LIST1 args ; "]" ;
+        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
+      let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in
+      { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
+    ] ]
+  ;
+  fun_rule:
+    [ [ "["; s = STRING; l = LIST0 args; "]";
+        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
+      let () = if s = "" then failwith "Command name is empty." in
+      let b = <:expr< $e$ >> in
       { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
       | "[" ; "-" ; l = LIST1 args ; "]" ;
         d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      let b = <:expr< fun () -> $e$ >> in
+      let b = <:expr< $e$ >> in
       { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
     ] ]
   ;
   classifier:
-    [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun () -> $c$>> ] ]
+    [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun loc -> $c$>> ] ]
   ;
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let e = parse_user_entry e "" in
-        ExtNonTerminal (e, s)
+        ExtNonTerminal (e, Some s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let e = parse_user_entry e sep in
-        ExtNonTerminal (e, s)
+        ExtNonTerminal (e, Some s)
+      | e = LIDENT ->
+        let e = parse_user_entry e "" in
+        ExtNonTerminal (e, None)
       | s = STRING ->
         ExtTerminal s
     ] ]