Merge PR #6496: Generate typed generic code from ltac macros

13 files changed, 309 insertions, 224 deletions

diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 6c072e36a..525be6432 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -13,15 +13,6 @@
 open Q_util
 open Argextend
 
-(** 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 plugin_name = <:expr< __coq_plugin_name >>
 
 let mlexpr_of_ident id =
@@ -29,112 +20,33 @@ let mlexpr_of_ident id =
   let id = "$" ^ id in
   <:expr< Names.Id.of_string_soft $str:id$ >>
 
-let rec make_patt = function
-  | [] -> <:patt< [] >>
-  | ExtNonTerminal (_, Some 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, Some 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,
-   ploc_vala None,
-   make_let false e pt)
-
-let make_fun_clauses loc s l =
-  let map c = 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< Tacarg.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 (Loc.tag ( $mlexpr_of_symbol g$ , $mlexpr_of_option 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) -> p
-  | _ -> assert false
-
-let declare_tactic loc tacname ~level clause = match clause 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_name mlexpr_of_ident) vars in
-  let entry = mlexpr_of_string tacname 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 = make_fun loc [patt, ploc_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 (Loc.tag ( $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 tacname in
-  let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
-  let gl = mlexpr_of_clause clause in
-  let level = mlexpr_of_int level in
-  let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ ~{ level = $level$ } $gl$ >> in
-  declare_str_items loc
-    [ <:str_item< do {
-        Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc tacname clause$);
-        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
 
@@ -146,13 +58,17 @@ EXTEND
         OPT "|"; l = LIST1 tacrule SEP "|";
         "END" ->
         let level = match level with Some i -> int_of_string i | None -> 0 in
-         declare_tactic loc s ~level l ] ]
+        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; "]";
-        "->"; "["; e = Pcaml.expr; "]" -> (l,e)
+        "->"; "["; e = Pcaml.expr; "]" ->
+         <:expr< TyML($mlexpr_of_clause l$, $binders_of_clause e l$) >>
     ] ]
   ;
+
   tacargs:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let e = parse_user_entry e "" in
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index 24ee0042b..a2872d07f 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -12,7 +12,6 @@
 
 open Q_util
 open Argextend
-open Tacextend
 
 type rule = {
   r_head : string option;
@@ -27,6 +26,21 @@ 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, Some p) :: l ->
diff --git a/intf/extend.ml b/intf/extend.ml
index 10c9b3dc1..734b859f6 100644
--- a/intf/extend.ml
+++ b/intf/extend.ml
@@ -85,6 +85,15 @@ type 'a user_symbol =
 | Uentry of 'a
 | Uentryl of 'a * int
 
+type ('a,'b,'c) ty_user_symbol =
+| TUlist1 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
+| TUlist1sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
+| TUlist0 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol
+| TUlist0sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol
+| TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol
+| TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol
+| TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol
+
 (** {5 Type-safe grammar extension} *)
 
 type ('self, 'a) symbol =
diff --git a/lib/genarg.ml b/lib/genarg.ml
index cf3a2bee7..209d1b271 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -174,19 +174,22 @@ sig
   val default : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) obj option
 end
 
+let get_arg_tag = function
+| ExtraArg s -> s
+| _ -> assert false
+
 module Register (M : GenObj) =
 struct
   module GenMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) M.obj end)
   let arg0_map = ref GenMap.empty
 
-  let register0 arg f = match arg with
-  | ExtraArg s ->
+  let register0 arg f =
+    let s = get_arg_tag arg in
     if GenMap.mem s !arg0_map then
       let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) ++ str "." in
       CErrors.anomaly msg
     else
       arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map
-  | _ -> assert false
 
   let get_obj0 name =
     try
@@ -199,8 +202,6 @@ struct
 
   (** For now, the following function is quite dummy and should only be applied
       to an extra argument type, otherwise, it will badly fail. *)
-  let obj t = match t with
-  | ExtraArg s -> get_obj0 s
-  | _ -> assert false
+  let obj t = get_obj0 @@ get_arg_tag t
 
 end
diff --git a/lib/genarg.mli b/lib/genarg.mli
index d49cb334a..bb85f99e3 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -159,6 +159,9 @@ val unquote : ('a, 'co) abstract_argument_type -> argument_type
 
   This is boilerplate code used here and there in the code of Coq. *)
 
+val get_arg_tag : ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c) ArgT.tag
+(** Works only on base objects (ExtraArg), otherwise fails badly. *)
+
 module type GenObj =
 sig
   type ('raw, 'glb, 'top) obj
diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4
index b3bcc9984..2251a6620 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
@@ -15,6 +15,7 @@
 (************************************************************************)
 
 open Eqdecide
+open Stdarg
 
 DECLARE PLUGIN "ltac_plugin"
 
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 4665ff9ed..2c7ebb745 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -16,6 +16,7 @@ open Misctypes
 open Genarg
 open Stdarg
 open Geninterp
+open Pp
 
 exception CannotCoerceTo of string
 
@@ -94,6 +95,38 @@ let to_option v = prj Val.typ_opt v
 
 let to_pair v = prj Val.typ_pair v
 
+let cast_error wit v =
+  let pr_v = Pptactic.pr_value Pptactic.ltop v in
+  let Val.Dyn (tag, _) = v in
+  let tag = Val.pr tag in
+  CErrors.user_err (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
+    ++ str " while type " ++ Val.pr wit ++ str " was expected.")
+
+let unbox wit v ans = match ans with
+| None -> cast_error wit v
+| Some x -> x
+
+let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with
+| Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.typ_list v (to_list v))
+| Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.typ_opt v (to_option v))
+| Val.Pair (tag1, tag2) ->
+  let (x, y) = unbox Val.typ_pair v (to_pair v) in
+  (prj tag1 x, prj tag2 y)
+| Val.Base t ->
+  let Val.Dyn (t', x) = v in
+  match Val.eq t t' with
+  | None -> cast_error t v
+  | Some Refl -> x
+let rec tag_of_arg : type a b c. (a, b, c) genarg_type -> c Val.tag = fun wit -> match wit with
+| ExtraArg _ -> Geninterp.val_tag (topwit wit)
+| ListArg t -> Val.List (tag_of_arg t)
+| OptArg t -> Val.Opt (tag_of_arg t)
+| PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2)
+
+let val_cast arg v = prj (tag_of_arg arg) v
+
+let cast (Topwit wit) v = val_cast wit v
+
 end
 
 let is_variable env id =
@@ -334,3 +367,46 @@ let coerce_to_int_or_var_list v =
   | Some l ->
     let map n = ArgArg (coerce_to_int n) in
     List.map map l
+
+(** Abstract application, to print ltac functions *)
+type appl =
+  | UnnamedAppl (** For generic applications: nothing is printed *)
+  | GlbAppl of (Names.KerName.t * Val.t list) list
+       (** For calls to global constants, some may alias other. *)
+
+(* Values for interpretation *)
+type tacvalue =
+  | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t *
+      Name.t list * Tacexpr.glob_tactic_expr
+  | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
+
+let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
+  let wit = Genarg.create_arg "tacvalue" in
+  let () = register_val0 wit None in
+  let () = Genprint.register_val_print0 (base_val_typ wit)
+             (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in
+  wit
+
+let pr_argument_type arg =
+  let Val.Dyn (tag, _) = arg in
+  Val.pr tag
+
+(** TODO: unify printing of generic Ltac values in case of coercion failure. *)
+
+(* Displays a value *)
+let pr_value env v =
+  let pr_with_env pr =
+    match env with
+    | Some (env,sigma) -> pr env sigma
+    | None -> str "a value of type" ++ spc () ++ pr_argument_type v in
+  let open Genprint in
+  match generic_val_print v with
+  | TopPrinterBasic pr -> pr ()
+  | TopPrinterNeedsContext pr -> pr_with_env pr
+  | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
+     pr_with_env (fun env sigma -> printer env sigma default_already_surrounded)
+
+let error_ltac_variable ?loc id env v s =
+   CErrors.user_err ?loc  (str "Ltac variable " ++ Id.print id ++
+   strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
+   strbrk "which cannot be coerced to " ++ str s ++ str".")
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index ce05d70e8..1fa5e3c07 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -42,6 +42,7 @@ sig
   val to_list : t -> t list option
   val to_option : t -> t option option
   val to_pair : t -> (t * t) option
+  val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a
 end
 
 (** {5 Coercion functions} *)
@@ -92,3 +93,21 @@ val coerce_to_int_or_var_list : Value.t -> int or_var list
 val wit_constr_context : (Empty.t, Empty.t, EConstr.constr) genarg_type
 
 val wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) genarg_type
+
+val error_ltac_variable : ?loc:Loc.t -> Id.t ->
+  (Environ.env * Evd.evar_map) option -> Value.t -> string -> 'a
+
+(** Abstract application, to print ltac functions *)
+type appl =
+  | UnnamedAppl (** For generic applications: nothing is printed *)
+  | GlbAppl of (Names.KerName.t * Val.t list) list
+       (** For calls to global constants, some may alias other. *)
+
+type tacvalue =
+  | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t *
+      Name.t list * Tacexpr.glob_tactic_expr
+  | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
+
+val wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type
+
+val pr_value : (Environ.env * Evd.evar_map) option -> Geninterp.Val.t -> Pp.t
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 42f2abd73..566fc2873 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -554,3 +554,138 @@ let () =
     AnyEntry Pltac.tactic_arg;
   ] in
   register_grammars_by_name "tactic" entries
+
+type _ ty_sig =
+| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
+| TyIdent : string * 'r ty_sig -> 'r ty_sig
+| TyArg :
+  (('a, 'b, 'c) Extend.ty_user_symbol * Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig
+| TyAnonArg :
+  ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig
+
+type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
+
+let rec untype_user_symbol : type a b c. (a,b,c) ty_user_symbol -> Genarg.ArgT.any user_symbol = fun tu ->
+  match tu with
+  | TUlist1 l -> Ulist1(untype_user_symbol l)
+  | TUlist1sep(l,s) -> Ulist1sep(untype_user_symbol l, s)
+  | TUlist0 l -> Ulist0(untype_user_symbol l)
+  | TUlist0sep(l,s) -> Ulist0sep(untype_user_symbol l, s)
+  | TUopt(o) -> Uopt(untype_user_symbol o)
+  | TUentry a -> Uentry (Genarg.ArgT.Any a)
+  | TUentryl (a,i) -> Uentryl (Genarg.ArgT.Any a,i)
+
+let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list =
+  fun sign -> match sign with
+  | TyNil -> []
+  | TyIdent (s, sig') -> TacTerm s :: clause_of_sign sig'
+  | TyArg ((loc,(a,id)),sig') ->
+    TacNonTerm (loc,(untype_user_symbol a,Some id)) :: clause_of_sign sig'
+  | TyAnonArg ((loc,a),sig') ->
+    TacNonTerm (loc,(untype_user_symbol a,None)) :: clause_of_sign sig'
+
+let clause_of_ty_ml = function
+  | TyML (t,_) -> clause_of_sign t
+
+let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function
+  | TUentry a -> ExtraArg a
+  | TUentryl (a,l) -> ExtraArg a
+  | TUopt(o) -> OptArg (prj o)
+  | TUlist1 l -> ListArg (prj l)
+  | TUlist1sep (l,_) -> ListArg (prj l)
+  | TUlist0 l -> ListArg (prj l)
+  | TUlist0sep (l,_) -> ListArg (prj l)
+
+let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic =
+  fun sign tac ->
+    match sign with
+    | TyNil ->
+      begin fun vals ist -> match vals with
+      | [] -> tac ist
+      | _ :: _ -> assert false
+      end
+    | TyIdent (s, sig') -> eval_sign sig' tac
+    | TyArg ((_loc,(a,id)), sig') ->
+      let f = eval_sign sig' in
+      begin fun tac vals ist -> match vals with
+      | [] -> assert false
+      | v :: vals ->
+        let v' = Taccoerce.Value.cast (topwit (prj a)) v in
+        f (tac v') vals ist
+      end tac
+    | TyAnonArg ((_loc,a), sig') -> eval_sign sig' tac
+
+let eval : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = function
+  | TyML (t,tac) -> eval_sign t tac
+
+let is_constr_entry = function
+| TUentry a -> Option.has_some @@ genarg_type_eq (ExtraArg a) Stdarg.wit_constr
+| _ -> false
+
+let rec only_constr : type a. a ty_sig -> bool = function
+| TyNil -> true
+| TyIdent(_,_) -> false
+| TyArg((_,(u,_)),s) -> if is_constr_entry u then only_constr s else false
+| TyAnonArg((_,u),s) -> if is_constr_entry u then only_constr s else false
+
+let rec mk_sign_vars : type a. a ty_sig -> Name.t list = function
+| TyNil -> []
+| TyIdent (_,s) -> mk_sign_vars s
+| TyArg((_,(_,name)),s) -> Name name :: mk_sign_vars s
+| TyAnonArg((_,_),s) -> Anonymous :: mk_sign_vars s
+
+let dummy_id = Id.of_string "_"
+
+let lift_constr_tac_to_ml_tac vars tac =
+  let tac _ ist = Proofview.Goal.enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Tacmach.New.project gl in
+    let map = function
+    | Anonymous -> None
+    | Name id ->
+      let c = Id.Map.find id ist.Geninterp.lfun in
+      try Some (Taccoerce.Value.of_constr @@ Taccoerce.coerce_to_closed_constr env c)
+      with Taccoerce.CannotCoerceTo ty ->
+        Taccoerce.error_ltac_variable dummy_id (Some (env,sigma)) c ty
+    in
+    let args = List.map_filter map vars in
+    tac args ist
+  end in
+  tac
+
+let tactic_extend plugin_name tacname ~level sign =
+  let open Tacexpr in
+  let ml_tactic_name =
+    { mltac_tactic = tacname;
+      mltac_plugin = plugin_name }
+  in
+  match sign with
+  | [TyML (TyIdent (name, s),tac) as ml_tac] when only_constr s ->
+  (** 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_name mlexpr_of_ident) vars in
+       *)
+    let vars = mk_sign_vars s in
+    let ml = { Tacexpr.mltac_name = ml_tactic_name; Tacexpr.mltac_index = 0 } in
+    let tac = match s with
+    | TyNil -> eval ml_tac
+    (** 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]. *)
+    | _ -> lift_constr_tac_to_ml_tac vars (eval ml_tac)
+    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 = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in
+    let id = Names.Id.of_string name in
+    let obj () = Tacenv.register_ltac true false id body in
+    let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in
+    Mltop.declare_cache_obj obj plugin_name
+  | _ ->
+  let obj () = add_ml_tactic_notation ml_tactic_name ~level (List.map clause_of_ty_ml sign) in
+  Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign);
+  Mltop.declare_cache_obj obj plugin_name
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 02e2f0f60..3f804ee8d 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -67,3 +67,15 @@ val print_ltacs : unit -> unit
 
 val print_located_tactic : Libnames.reference -> unit
 (** Display the absolute name of a tactic. *)
+
+type _ ty_sig =
+| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
+| TyIdent : string * 'r ty_sig -> 'r ty_sig
+| TyArg :
+  (('a, 'b, 'c) Extend.ty_user_symbol * Names.Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig
+| TyAnonArg :
+  ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig
+
+type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
+
+val tactic_extend : string -> string -> level:Int.t -> ty_ml list -> unit
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index cd9d9bac2..991afe9c6 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -79,9 +79,6 @@ let out_gen wit v =
 
 let val_tag wit = val_tag (topwit wit)
 
-let base_val_typ wit =
-  match val_tag wit with Val.Base t -> t | _ -> anomaly (str "Not a base val.")
-
 let pr_argument_type arg =
   let Val.Dyn (tag, _) = arg in
   Val.pr tag
@@ -93,11 +90,6 @@ let safe_msgnl s =
 
 type value = Val.t
 
-(** Abstract application, to print ltac functions *)
-type appl =
-  | UnnamedAppl (** For generic applications: nothing is printed *)
-  | GlbAppl of (Names.KerName.t * Val.t list) list
-       (** For calls to global constants, some may alias other. *)
 let push_appl appl args =
   match appl with
   | UnnamedAppl -> UnnamedAppl
@@ -121,19 +113,6 @@ let combine_appl appl1 appl2 =
   | UnnamedAppl,a | a,UnnamedAppl -> a
   | GlbAppl l1 , GlbAppl l2 -> GlbAppl (l2@l1)
 
-(* Values for interpretation *)
-type tacvalue =
-  | VFun of appl*ltac_trace * value Id.Map.t *
-      Name.t list * glob_tactic_expr
-  | VRec of value Id.Map.t ref * glob_tactic_expr
-
-let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
-  let wit = Genarg.create_arg "tacvalue" in
-  let () = register_val0 wit None in
-  let () = Genprint.register_val_print0 (base_val_typ wit)
-             (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in
-  wit
-
 let of_tacvalue v = in_gen (topwit wit_tacvalue) v
 let to_tacvalue v = out_gen (topwit wit_tacvalue) v
 
@@ -169,39 +148,6 @@ module Value = struct
     let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
     of_tacvalue closure
 
-  let cast_error wit v =
-    let pr_v = Pptactic.pr_value Pptactic.ltop v in
-    let Val.Dyn (tag, _) = v in
-    let tag = Val.pr tag in
-    user_err  (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
-      ++ str " while type " ++ Val.pr wit ++ str " was expected.")
-
-  let unbox wit v ans = match ans with
-  | None -> cast_error wit v
-  | Some x -> x
-
-  let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with
-  | Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.typ_list v (to_list v))
-  | Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.typ_opt v (to_option v))
-  | Val.Pair (tag1, tag2) ->
-    let (x, y) = unbox Val.typ_pair v (to_pair v) in
-    (prj tag1 x, prj tag2 y)
-  | Val.Base t ->
-    let Val.Dyn (t', x) = v in
-    match Val.eq t t' with
-    | None -> cast_error t v
-    | Some Refl -> x
-
-  let rec tag_of_arg : type a b c. (a, b, c) genarg_type -> c Val.tag = fun wit -> match wit with
-  | ExtraArg _ -> val_tag wit
-  | ListArg t -> Val.List (tag_of_arg t)
-  | OptArg t -> Val.Opt (tag_of_arg t)
-  | PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2)
-
-  let val_cast arg v = prj (tag_of_arg arg) v
-
-  let cast (Topwit wit) v = val_cast wit v
-
 end
 
 let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
@@ -233,21 +179,6 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with
 | None -> DebugOff
 | Some level -> level
 
-(** TODO: unify printing of generic Ltac values in case of coercion failure. *)
-
-(* Displays a value *)
-let pr_value env v =
-  let pr_with_env pr =
-    match env with
-    | Some (env,sigma) -> pr env sigma
-    | None -> str "a value of type" ++ spc () ++ pr_argument_type v in
-  let open Genprint in
-  match generic_val_print v with
-  | TopPrinterBasic pr -> pr ()
-  | TopPrinterNeedsContext pr -> pr_with_env pr
-  | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
-     pr_with_env (fun env sigma -> printer env sigma default_already_surrounded)
-
 let pr_closure env ist body =
   let pp_body = Pptactic.pr_glob_tactic env body in
   let pr_sep () = fnl () in
@@ -360,15 +291,11 @@ let debugging_exception_step ist signal_anomaly e pp =
   debugging_step ist (fun () ->
     pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e)
 
-let error_ltac_variable ?loc id env v s =
-   user_err ?loc  (str "Ltac variable " ++ Id.print id ++
-   strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
-   strbrk "which cannot be coerced to " ++ str s ++ str".")
-
 (* Raise Not_found if not in interpretation sign *)
 let try_interp_ltac_var coerce ist env {loc;v=id} =
   let v = Id.Map.find id ist.lfun in
-  try coerce v with CannotCoerceTo s -> error_ltac_variable ?loc id env v s
+  try coerce v with CannotCoerceTo s ->
+    Taccoerce.error_ltac_variable ?loc id env v s
 
 let interp_ltac_var coerce ist env locid =
   try try_interp_ltac_var coerce ist env locid
@@ -2090,27 +2017,6 @@ let _ =
   in
   Pretyping.register_constr_interp0 wit_tactic eval
 
-(** Used in tactic extension **)
-
-let dummy_id = Id.of_string "_"
-
-let lift_constr_tac_to_ml_tac vars tac =
-  let tac _ ist = Proofview.Goal.enter begin fun gl ->
-    let env = Proofview.Goal.env gl in
-    let sigma = project gl in
-    let map = function
-    | Anonymous -> None
-    | Name id ->
-      let c = Id.Map.find id ist.lfun in
-      try Some (coerce_to_closed_constr env c)
-      with CannotCoerceTo ty ->
-        error_ltac_variable dummy_id (Some (env,sigma)) c ty
-    in
-    let args = List.map_filter map vars in
-    tac args ist
-  end in
-  tac
-
 let vernac_debug b =
   set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
 
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 3f3b8e555..bd44bdbea 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -133,13 +133,5 @@ val interp_int : interp_sign -> lident -> int
 
 val interp_int_or_var : interp_sign -> int or_var -> int
 
-val error_ltac_variable : ?loc:Loc.t -> Id.t ->
-  (Environ.env * Evd.evar_map) option -> value -> string -> 'a
-
-(** Transforms a constr-expecting tactic into a tactic finding its arguments in
-    the Ltac environment according to the given names. *)
-val lift_constr_tac_to_ml_tac : Name.t list ->
-  (constr list -> Geninterp.interp_sign -> unit Proofview.tactic) -> Tacenv.ml_tactic
-
 val default_ist : unit -> Geninterp.interp_sign
 (** Empty ist with debug set on the current value. *)
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index c8112eaa9..4ac49adb9 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Ltac_plugin
+open Stdarg
 
 DECLARE PLUGIN "nsatz_plugin"