Change the toplevel representation of Ltac values to an untyped one.

This brings the evaluation model of Ltac closer to those of usual languages, and
further allows the integration of static typing in the long run. More precisely,
toplevel constructed values such as lists and the like do not carry anymore the
type of the underlying data they contain.

This is mostly an API change, as it did not break any contrib outside of mathcomp.

41 files changed, 391 insertions, 375 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 9f25ba55e7..5d10f54fb2 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -146,6 +146,8 @@ Typeclasses_errors
 Logic_monad
 Proofview_monad
 Proofview
+Ftactic
+Geninterp
 Typeclasses
 Detyping
 Indrec
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 29ea08e025..f9c1971a82 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -467,8 +467,8 @@ let pp_generic_argument arg =
   pp(str"<genarg:"++pr_argument_type(genarg_tag arg)++str">")
 
 let prgenarginfo arg =
-  let Val.Dyn (tag, _) = arg in
-  let tpe = Val.pr tag in
+  let Geninterp.Val.Dyn (tag, _) = arg in
+  let tpe = Geninterp.Val.pr tag in
   (** FIXME *)
 (*   try *)
 (*     let data = Pptactic.pr_top_generic (Global.env ()) arg in *)
diff --git a/engine/engine.mllib b/engine/engine.mllib
index 70b74edca3..9ce5af8195 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -7,3 +7,5 @@ Sigma
 Proofview_monad
 Evarutil
 Proofview
+Ftactic
+Geninterp
diff --git a/tactics/ftactic.ml b/engine/ftactic.ml
index 588709873e..588709873e 100644
--- a/tactics/ftactic.ml
+++ b/engine/ftactic.ml
diff --git a/tactics/ftactic.mli b/engine/ftactic.mli
index 19041f1698..19041f1698 100644
--- a/tactics/ftactic.mli
+++ b/engine/ftactic.mli
diff --git a/engine/geninterp.ml b/engine/geninterp.ml
new file mode 100644
index 0000000000..45b0aa2316
--- /dev/null
+++ b/engine/geninterp.ml
@@ -0,0 +1,98 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+open Names
+open Genarg
+
+module TacStore = Store.Make(struct end)
+
+(** Dynamic toplevel values *)
+
+module ValT = Dyn.Make(struct end)
+
+module Val =
+struct
+
+  type 'a typ = 'a ValT.tag
+
+  type _ tag =
+  | Base : 'a typ -> 'a tag
+  | List : 'a tag -> 'a list tag
+  | Opt : 'a tag -> 'a option tag
+  | Pair : 'a tag * 'b tag -> ('a * 'b) tag
+
+  type t = Dyn : 'a typ * 'a -> t
+
+  let eq = ValT.eq
+  let repr = ValT.repr
+  let create = ValT.create
+
+  let rec pr : type a. a typ -> Pp.std_ppcmds = fun t -> Pp.str (repr t)
+
+  let typ_list = ValT.create "list"
+  let typ_opt = ValT.create "option"
+  let typ_pair = ValT.create "pair"
+
+  let rec inject : type a. a tag -> a -> t = fun tag x -> match tag with
+  | Base t -> Dyn (t, x)
+  | List tag -> Dyn (typ_list, List.map (fun x -> inject tag x) x)
+  | Opt tag -> Dyn (typ_opt, Option.map (fun x -> inject tag x) x)
+  | Pair (tag1, tag2) ->
+    Dyn (typ_pair, (inject tag1 (fst x), inject tag2 (snd x)))
+
+end
+
+module ValReprObj =
+struct
+  type ('raw, 'glb, 'top) obj = 'top Val.tag
+  let name = "valrepr"
+  let default _ = None
+end
+
+module ValRepr = Register(ValReprObj)
+
+let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function
+| ListArg t -> Val.List (val_tag t)
+| OptArg t -> Val.Opt (val_tag t)
+| PairArg (t1, t2) -> Val.Pair (val_tag t1, val_tag t2)
+| ExtraArg s -> ValRepr.obj (ExtraArg s)
+
+let val_tag = function Topwit t -> val_tag t
+
+let register_val0 wit tag =
+  let tag = match tag with
+  | None ->
+    let name = match wit with
+    | ExtraArg s -> ArgT.repr s
+    | _ -> assert false
+    in
+    Val.Base (Val.create name)
+  | Some tag -> tag
+  in
+  ValRepr.register0 wit tag
+
+(** Interpretation functions *)
+
+type interp_sign = {
+  lfun : Val.t Id.Map.t;
+  extra : TacStore.t }
+
+type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
+
+module InterpObj =
+struct
+  type ('raw, 'glb, 'top) obj = ('glb, Val.t) interp_fun
+  let name = "interp"
+  let default _ = None
+end
+
+module Interp = Register(InterpObj)
+
+let interp = Interp.obj
+
+let register_interp0 = Interp.register0
diff --git a/engine/geninterp.mli b/engine/geninterp.mli
new file mode 100644
index 0000000000..42e1e3784c
--- /dev/null
+++ b/engine/geninterp.mli
@@ -0,0 +1,67 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** Interpretation functions for generic arguments. *)
+
+open Names
+open Genarg
+
+(** {6 Dynamic toplevel values} *)
+
+module Val :
+sig
+  type 'a typ
+
+  val create : string -> 'a typ
+
+  type _ tag =
+  | Base : 'a typ -> 'a tag
+  | List : 'a tag -> 'a list tag
+  | Opt : 'a tag -> 'a option tag
+  | Pair : 'a tag * 'b tag -> ('a * 'b) tag
+
+  type t = Dyn : 'a typ * 'a -> t
+
+  val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option
+  val repr : 'a typ -> string
+  val pr : 'a typ -> Pp.std_ppcmds
+
+  val typ_list : t list typ
+  val typ_opt : t option typ
+  val typ_pair : (t * t) typ
+
+  val inject : 'a tag -> 'a -> t
+
+end
+(** Dynamic types for toplevel values. While the generic types permit to relate
+    objects at various levels of interpretation, toplevel values are wearing
+    their own type regardless of where they came from. This allows to use the
+    same runtime representation for several generic types. *)
+
+val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag
+(** Retrieve the dynamic type associated to a toplevel genarg. *)
+
+val register_val0 : ('raw, 'glb, 'top) genarg_type -> 'top Val.tag option -> unit
+(** Register the representation of a generic argument. If no tag is given as
+    argument, a new fresh tag with the same name as the argument is associated
+    to the generic type. *)
+
+(** {6 Interpretation functions} *)
+
+module TacStore : Store.S
+
+type interp_sign = {
+  lfun : Val.t Id.Map.t;
+  extra : TacStore.t }
+
+type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
+
+val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun
+
+val register_interp0 :
+  ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun -> unit
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index dca3e1656f..3b7e180c6f 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -88,6 +88,7 @@ let check_type prefix s = function
 | Some _ -> warning_redundant prefix s
 
 let declare_tactic_argument loc s (typ, f, g, h) cl =
+  let se = mlexpr_of_string s in
   let rawtyp, rawpr, globtyp, globpr, typ, pr = match typ with
     | `Uniform (typ, pr) ->
       let typ = get_type "" s typ in
@@ -118,19 +119,21 @@ let declare_tactic_argument loc s (typ, f, g, h) cl =
   let interp = match f with
     | None ->
       begin match globtyp with
-      | None -> <:expr< fun ist v -> Ftactic.return v >>
+      | None ->
+        let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in
+        <:expr< fun ist v -> Ftactic.return (Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v) >>
       | Some globtyp ->
         <:expr< fun ist x ->
-          Ftactic.bind
-            (Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x))
-            (fun v -> Ftactic.return (Tacinterp.Value.cast $make_topwit loc globtyp$ v)) >>
+          Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x) >>
       end
     | Some f ->
       (** Compatibility layer, TODO: remove me *)
+      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 ->
           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)
         }
       >> in
@@ -147,20 +150,15 @@ let declare_tactic_argument loc s (typ, f, g, h) cl =
     | Some f -> <:expr< $lid:f$>> in
   let dyn = match typ with
   | None -> <:expr< None >>
-  | Some typ ->
-    if is_self s typ then <:expr< None >>
-    else <:expr< Some (Genarg.val_tag $make_topwit loc typ$) >>
+  | Some typ -> <:expr< Some (Geninterp.val_tag $make_topwit loc typ$) >>
   in
-  let se = mlexpr_of_string s in
   let wit = <:expr< $lid:"wit_"^s$ >> in
   declare_str_items loc
-   [ <:str_item<
-      value ($lid:"wit_"^s$) =
-        let dyn = $dyn$ in
-        Genarg.make0 ?dyn $se$ >>;
+   [ <:str_item< value ($lid:"wit_"^s$) = Genarg.make0 $se$ >>;
      <:str_item< Genintern.register_intern0 $wit$ $glob$ >>;
      <:str_item< Genintern.register_subst0 $wit$ $subst$ >>;
      <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>;
+     <:str_item< Geninterp.register_val0 $wit$ $dyn$ >>;
      make_extend loc s cl wit;
      <:str_item< do {
       Pptactic.declare_extra_genarg_pprule
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 46be0b8a1f..b8f97e77c3 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -11,6 +11,12 @@ open Tacexpr
 open Term
 open Misctypes
 open Genarg
+open Geninterp
+
+let make0 ?dyn name =
+  let wit = Genarg.make0 name in
+  let () = Geninterp.register_val0 wit dyn in
+  wit
 
 (** This is a hack for now, to break the dependency of Genarg on constr-related
     types. We should use dedicated functions someday. *)
@@ -20,50 +26,47 @@ let loc_of_or_by_notation f = function
   | ByNotation (loc,s,_) -> loc
 
 let wit_int_or_var =
-  Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var"
+  make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var"
 
 let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type =
-  Genarg.make0 "intropattern"
+  make0 "intropattern"
 
 let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
-  Genarg.make0 "tactic"
+  make0 "tactic"
 
-let wit_ltac = Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac"
+let wit_ltac = make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac"
 
 let wit_ident =
-  Genarg.make0 "ident"
+  make0 "ident"
 
 let wit_var =
-  Genarg.make0 ~dyn:(val_tag (topwit wit_ident)) "var"
-
-let wit_ref = Genarg.make0 "ref"
+  make0 ~dyn:(val_tag (topwit wit_ident)) "var"
 
-let wit_quant_hyp = Genarg.make0 "quant_hyp"
+let wit_ref = make0 "ref"
 
-let wit_sort : (glob_sort, glob_sort, sorts) genarg_type =
-  Genarg.make0 "sort"
+let wit_quant_hyp = make0 "quant_hyp"
 
 let wit_constr =
-  Genarg.make0 "constr"
+  make0 "constr"
 
 let wit_constr_may_eval =
-  Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) "constr_may_eval"
+  make0 ~dyn:(val_tag (topwit wit_constr)) "constr_may_eval"
 
-let wit_uconstr = Genarg.make0 "uconstr"
+let wit_uconstr = make0 "uconstr"
 
-let wit_open_constr = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
+let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
 
-let wit_constr_with_bindings = Genarg.make0 "constr_with_bindings"
+let wit_constr_with_bindings = make0 "constr_with_bindings"
 
-let wit_bindings = Genarg.make0 "bindings"
+let wit_bindings = make0 "bindings"
 
 let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type =
-  Genarg.make0 "hyp_location_flag"
+  make0 "hyp_location_flag"
 
-let wit_red_expr = Genarg.make0 "redexpr"
+let wit_red_expr = make0 "redexpr"
 
 let wit_clause_dft_concl  =
-  Genarg.make0 "clause_dft_concl"
+  make0 "clause_dft_concl"
 
 (** Aliases *)
 
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index d38b1183c5..70c9c0de2c 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -38,15 +38,8 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen
 
 val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
 
-val wit_sort : (glob_sort, glob_sort, sorts) genarg_type
-
 val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
 
-val wit_constr_may_eval :
-  ((constr_expr,reference or_by_notation,constr_expr) may_eval,
-  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
-  constr) genarg_type
-
 val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
 
 val wit_open_constr :
@@ -62,14 +55,12 @@ val wit_bindings :
   glob_constr_and_expr bindings,
   constr bindings delayed_open) genarg_type
 
-val wit_hyp_location_flag : Locus.hyp_location_flag uniform_genarg_type
-
 val wit_red_expr :
   ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
   (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
 
-val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type
+val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_type
 
 (** [wit_ltac] is subtly different from [wit_tactic]: they only change for their
     toplevel interpretation. The one of [wit_ltac] forces the tactic and
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 244cdd0a70..2a7d52e3af 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -7,6 +7,12 @@
 (************************************************************************)
 
 open Genarg
+open Geninterp
+
+let make0 ?dyn name =
+  let wit = Genarg.make0 name in
+  let () = register_val0 wit dyn in
+  wit
 
 let wit_unit : unit uniform_genarg_type =
   make0 "unit"
@@ -21,7 +27,7 @@ let wit_string : string uniform_genarg_type =
   make0 "string"
 
 let wit_pre_ident : string uniform_genarg_type =
-  make0 "preident"
+  make0 ~dyn:(val_tag (topwit wit_string)) "preident"
 
 (** Aliases for compatibility *)
 
diff --git a/lib/genarg.ml b/lib/genarg.ml
index ef0de89afb..69408fb1a5 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -9,7 +9,6 @@
 open Pp
 open Util
 
-module ValT = Dyn.Make(struct end)
 module ArgT =
 struct
   module DYN = Dyn.Make(struct end)
@@ -25,52 +24,6 @@ struct
     Some (Any (Obj.magic t)) (** All created tags are made of triples *)
 end
 
-module Val =
-struct
-
-  type 'a typ = 'a ValT.tag
-
-  type _ tag =
-  | Base : 'a typ -> 'a tag
-  | List : 'a tag -> 'a list tag
-  | Opt : 'a tag -> 'a option tag
-  | Pair : 'a tag * 'b tag -> ('a * 'b) tag
-
-  type t = Dyn : 'a tag * 'a -> t
-
-  let rec eq : type a b. a tag -> b tag -> (a, b) CSig.eq option =
-  fun t1 t2 -> match t1, t2 with
-  | Base t1, Base t2 -> ValT.eq t1 t2
-  | List t1, List t2 ->
-    begin match eq t1 t2 with
-    | None -> None
-    | Some Refl -> Some Refl
-    end
-  | Opt t1, Opt t2 ->
-    begin match eq t1 t2 with
-    | None -> None
-    | Some Refl -> Some Refl
-    end
-  | Pair (t1, u1), Pair (t2, u2) ->
-    begin match eq t1 t2 with
-    | None -> None
-    | Some Refl ->
-      match eq u1 u2 with
-      | None -> None
-      | Some Refl -> Some Refl
-    end
-  | _ -> None
-
-  let repr = ValT.repr
-
-  let rec pr : type a. a tag -> std_ppcmds = function
-  | Base t -> str (repr t)
-  | List t -> pr t ++ spc () ++ str "list"
-  | Opt t -> pr t ++ spc () ++ str "option"
-  | Pair (t1, t2) -> str "(" ++ pr t1 ++ str " * " ++ pr t2 ++ str ")"
-
-end
-
 type (_, _, _) genarg_type =
 | ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type
 | ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
@@ -202,36 +155,14 @@ struct
   include ArgT.Map(struct type 'a t = 'a pack end)
 end
 
-type ('raw, 'glb, 'top) load = {
-  dyn : 'top Val.tag;
-}
-
-module LoadMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) load end)
-
-let arg0_map = ref LoadMap.empty
-
-let create_arg ?dyn name =
+let create_arg name =
   match ArgT.name name with
+  | None -> ExtraArg (ArgT.create name)
   | Some _ ->
     Errors.anomaly (str "generic argument already declared: " ++ str name)
-  | None ->
-    let dyn = match dyn with None -> Val.Base (ValT.create name) | Some dyn -> dyn in
-    let obj = LoadMap.Pack { dyn; } in
-    let name = ArgT.create name in
-    let () = arg0_map := LoadMap.add name obj !arg0_map in
-    ExtraArg name
 
 let make0 = create_arg
 
-let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function
-| ListArg t -> Val.List (val_tag t)
-| OptArg t -> Val.Opt (val_tag t)
-| PairArg (t1, t2) -> Val.Pair (val_tag t1, val_tag t2)
-| ExtraArg s ->
-  match LoadMap.find s !arg0_map with LoadMap.Pack obj -> obj.dyn
-
-let val_tag = function Topwit t -> val_tag t
-
 (** Registering genarg-manipulating functions *)
 
 module type GenObj =
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 93665fd45d..b8bb6af04a 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -86,36 +86,14 @@ type (_, _, _) genarg_type =
 (** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized
     one, and ['top] the internalized one. *)
 
-module Val :
-sig
-  type 'a typ
-
-  type _ tag =
-  | Base : 'a typ -> 'a tag
-  | List : 'a tag -> 'a list tag
-  | Opt : 'a tag -> 'a option tag
-  | Pair : 'a tag * 'b tag -> ('a * 'b) tag
-
-  type t = Dyn : 'a tag * 'a -> t
-
-  val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
-  val repr : 'a typ -> string
-  val pr : 'a tag -> Pp.std_ppcmds
-
-end
-(** Dynamic types for toplevel values. While the generic types permit to relate
-    objects at various levels of interpretation, toplevel values are wearing
-    their own type regardless of where they came from. This allows to use the
-    same runtime representation for several generic types. *)
-
 type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
 (** Alias for concision when the three types agree. *)
 
-val make0 : ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
+val make0 : string -> ('raw, 'glob, 'top) genarg_type
 (** Create a new generic type of argument: force to associate
     unique ML types at each of the three levels. *)
 
-val create_arg : ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
+val create_arg : string -> ('raw, 'glob, 'top) genarg_type
 (** Alias for [make0]. *)
 
 (** {5 Specialized types} *)
@@ -180,12 +158,6 @@ val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool
 (** [has_type v t] tells whether [v] has type [t]. If true, it ensures that
     [out_gen t v] will not raise a dynamic type exception. *)
 
-(** {6 Dynamic toplevel values} *)
-
-val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag
-(** Retrieve the dynamic type associated to a toplevel genarg. Only works for
-    ground generic arguments. *)
-
 (** {6 Type reification} *)
 
 type argument_type = ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type
diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli
index 14aa69875f..4d1d8ba7fe 100644
--- a/ltac/extraargs.mli
+++ b/ltac/extraargs.mli
@@ -54,7 +54,7 @@ val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
 val wit_by_arg_tac :
   (raw_tactic_expr option,
   glob_tactic_expr option,
-  Genarg.Val.t option) Genarg.genarg_type
+  Geninterp.Val.t option) Genarg.genarg_type
 
 val pr_by_arg_tac : 
   (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 0b475340e2..79f80260fa 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -258,7 +258,7 @@ END
 (**********************************************************************)
 (* Rewrite star                                                       *)
 
-let rewrite_star ist clause orient occs c (tac : Val.t option) =
+let rewrite_star ist clause orient occs c (tac : Geninterp.Val.t option) =
   let tac' = Option.map (fun t -> Tacinterp.tactic_of_value ist t, FirstSolved) tac in
   with_delayed_uconstr ist c
     (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true)
@@ -393,6 +393,12 @@ open Leminv
 
 let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater
 
+VERNAC ARGUMENT EXTEND sort
+| [ "Set" ] -> [ GSet ]
+| [ "Prop" ] -> [ GProp ]
+| [ "Type" ] -> [ GType [] ]
+END
+
 VERNAC COMMAND EXTEND DeriveInversionClear
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
   => [ seff na ]
@@ -938,10 +944,6 @@ type cmp =
 type 'i test =
   | Test of cmp * 'i * 'i
 
-let wit_cmp : (cmp,cmp,cmp) Genarg.genarg_type = Genarg.make0 "cmp"
-let wit_test : (int or_var test,int or_var test,int test) Genarg.genarg_type =
-  Genarg.make0 "tactest"
-
 let pr_cmp = function
   | Eq -> Pp.str"="
   | Lt -> Pp.str"<"
@@ -964,7 +966,7 @@ let pr_itest' _prc _prlc _prt = pr_itest
 
 
 
-ARGUMENT EXTEND comparison TYPED AS cmp PRINTED BY pr_cmp'
+ARGUMENT EXTEND comparison PRINTED BY pr_cmp'
 | [ "="  ] -> [ Eq ]
 | [ "<"  ] -> [ Lt ]
 | [ "<=" ] -> [ Le ]
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 97b2393a8d..cd8ce7e87a 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -613,8 +613,10 @@ let solve_remaining_by env sigma holes by =
     (** Only solve independent holes *)
     let indep = List.map_filter map holes in
     let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in
-    let solve_tac = Geninterp.generic_interp ist tac in
-    let solve_tac = Ftactic.run solve_tac (fun _ -> Proofview.tclUNIT ()) in
+    let solve_tac = match tac with
+    | Genarg.GenArg (Genarg.Glbwit tag, tac) ->
+      Ftactic.run (Geninterp.interp tag ist tac) (fun _ -> Proofview.tclUNIT ())
+    in
     let solve_tac = Tacticals.New.tclCOMPLETE solve_tac in
     let solve sigma evk =
       let evi =
diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml
index d2d3f3117f..f2dbb5b6c9 100644
--- a/ltac/tacenv.ml
+++ b/ltac/tacenv.ml
@@ -11,6 +11,7 @@ open Genarg
 open Pp
 open Names
 open Tacexpr
+open Geninterp
 
 (** Tactic notations (TacAlias) *)
 
@@ -32,7 +33,7 @@ let check_alias key = KNmap.mem key !alias_map
 (** ML tactic extensions (TacML) *)
 
 type ml_tactic =
-  Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic
+  Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic
 
 module MLName =
 struct
diff --git a/ltac/tacenv.mli b/ltac/tacenv.mli
index 88b54993b1..94e14223aa 100644
--- a/ltac/tacenv.mli
+++ b/ltac/tacenv.mli
@@ -9,6 +9,7 @@
 open Genarg
 open Names
 open Tacexpr
+open Geninterp
 
 (** This module centralizes the various ways of registering tactics. *)
 
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index 15589d5c4a..977c56f38b 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -800,7 +800,6 @@ let () =
   Genintern.register_intern0 wit_var (lift intern_hyp);
   Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
   Genintern.register_intern0 wit_ltac (lift intern_tactic_or_tacarg);
-  Genintern.register_intern0 wit_sort (fun ist s -> (ist, s));
   Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis);
   Genintern.register_intern0 wit_constr (fun ist c -> (ist,intern_constr ist c));
   Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c));
@@ -808,7 +807,6 @@ let () =
   Genintern.register_intern0 wit_red_expr (lift intern_red_expr);
   Genintern.register_intern0 wit_bindings (lift intern_bindings);
   Genintern.register_intern0 wit_constr_with_bindings (lift intern_constr_with_bindings);
-  Genintern.register_intern0 wit_constr_may_eval (lift intern_constr_may_eval);
   ()
 
 (***************************************************************************)
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 9b41a276b9..31bccd019d 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -30,6 +30,7 @@ open Term
 open Termops
 open Tacexpr
 open Genarg
+open Geninterp
 open Stdarg
 open Constrarg
 open Printer
@@ -48,18 +49,35 @@ let ltac_trace_info = Tactic_debug.ltac_trace_info
 
 let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
   let Val.Dyn (t, _) = v in
-  match Val.eq t (val_tag wit) with
+  let t' = match val_tag wit with
+  | Val.Base t' -> t'
+  | _ -> assert false (** not used in this module *)
+  in
+  match Val.eq t t' with
   | None -> false
   | Some Refl -> true
 
-let prj : type a. a Val.tag -> Val.t -> a option = fun t v ->
+let prj : type a. a Val.typ -> Val.t -> a option = fun t v ->
   let Val.Dyn (t', x) = v in
   match Val.eq t t' with
   | None -> None
   | Some Refl -> Some x
 
-let in_gen wit v = Val.Dyn (val_tag wit, v)
-let out_gen wit v = match prj (val_tag wit) v with None -> assert false | Some x -> x
+let in_list tag v =
+  let tag = match tag with Val.Base tag -> tag | _ -> assert false in
+  Val.Dyn (Val.typ_list, List.map (fun x -> Val.Dyn (tag, x)) v)
+let in_gen wit v =
+  let t = match val_tag wit with
+  | Val.Base t -> t
+  | _ -> assert false (** not used in this module *)
+  in
+  Val.Dyn (t, v)
+let out_gen wit v =
+  let t = match val_tag wit with
+  | Val.Base t -> t
+  | _ -> assert false (** not used in this module *)
+  in
+  match prj t v with None -> assert false | Some x -> x
 
 let val_tag wit = val_tag (topwit wit)
 
@@ -109,7 +127,9 @@ type tacvalue =
   | VRec of value Id.Map.t ref * glob_tactic_expr
 
 let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
-  Genarg.create_arg "tacvalue"
+  let wit = Genarg.create_arg "tacvalue" in
+  let () = register_val0 wit None in
+  wit
 
 let of_tacvalue v = in_gen (topwit wit_tacvalue) v
 let to_tacvalue v = out_gen (topwit wit_tacvalue) v
@@ -152,47 +172,31 @@ module Value = struct
     let Val.Dyn (tag, _) = v in
     let tag = Val.pr tag in
     errorlabstrm "" (str "Type error: value " ++ pr_v ++ str "is a " ++ tag
-      ++ str " while type " ++ Genarg.pr_argument_type (unquote (rawwit wit)) ++ str " was expected.")
+      ++ 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 prj : type a. a Val.tag -> Val.t -> a option = fun t v ->
+  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 -> None
-    | Some Refl -> Some x
+    | None -> cast_error t v
+    | Some Refl -> x
 
-  let try_prj wit v = match prj (val_tag wit) v with
-  | None -> cast_error wit v
-  | Some x -> 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 rec val_cast : type a b c. (a, b, c) genarg_type -> Val.t -> c =
-  fun wit v -> match wit with
-  | ExtraArg _ -> try_prj wit v
-  | ListArg t ->
-    let Val.Dyn (tag, v) = v in
-    begin match tag with
-    | Val.List tag ->
-      let map x = val_cast t (Val.Dyn (tag, x)) in
-      List.map map v
-    | _ -> cast_error wit (Val.Dyn (tag, v))
-    end
-  | OptArg t ->
-    let Val.Dyn (tag, v) = v in
-    begin match tag with
-    | Val.Opt tag ->
-      let map x = val_cast t (Val.Dyn (tag, x)) in
-      Option.map map v
-    | _ -> cast_error wit (Val.Dyn (tag, v))
-    end
-  | PairArg (t1, t2) ->
-    let Val.Dyn (tag, v) = v in
-    begin match tag with
-    | Val.Pair (tag1, tag2) ->
-      let (v1, v2) = v in
-      let v1 = Val.Dyn (tag1, v1) in
-      let v2 = Val.Dyn (tag2, v2) in
-      (val_cast t1 v1, val_cast t2 v2)
-    | _ -> cast_error wit (Val.Dyn (tag, v))
-    end
+  let rec val_cast arg v = prj (tag_of_arg arg) v
 
   let cast (Topwit wit) v = val_cast wit v
 
@@ -1144,17 +1148,6 @@ let rec read_match_rule lfun ist env sigma = function
   | [] -> []
 
 
-(* misc *)
-
-let interp_focussed wit f v =
-  Ftactic.nf_enter { enter = begin fun gl ->
-    let v = Genarg.out_gen (glbwit wit) v in
-    let env = Proofview.Goal.env gl in
-    let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
-    let v = in_gen (topwit wit) (f env sigma v) in
-    Ftactic.return v
-  end }
-
 (* Interprets an l-tac expression into a value *)
 let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftactic.t =
   (* The name [appl] of applied top-level Ltac names is ignored in
@@ -1553,30 +1546,23 @@ and interp_genarg ist x : Val.t Ftactic.t =
     let GenArg (Glbwit wit, x) = x in
     match wit with
     | ListArg wit ->
-      let map x =
-        interp_genarg ist (Genarg.in_gen (glbwit wit) x) >>= fun x ->
-        Ftactic.return (Value.cast (topwit wit) x)
-      in
+      let map x = interp_genarg ist (Genarg.in_gen (glbwit wit) x) in
       Ftactic.List.map map x >>= fun l ->
-      Ftactic.return (Value.of_list (val_tag wit) l)
+      Ftactic.return (Val.Dyn (Val.typ_list, l))
     | OptArg wit ->
-      let ans = match x with
-      | None -> Ftactic.return (Value.of_option (val_tag wit) None)
+      begin match x with
+      | None -> Ftactic.return (Val.Dyn (Val.typ_opt, None))
       | Some x ->
         interp_genarg ist (Genarg.in_gen (glbwit wit) x) >>= fun x ->
-        let x = Value.cast (topwit wit) x in
-        Ftactic.return (Value.of_option (val_tag wit) (Some x))
-      in
-      ans
+        Ftactic.return (Val.Dyn (Val.typ_opt, Some x))
+      end
     | PairArg (wit1, wit2) ->
       let (p, q) = x in
       interp_genarg ist (Genarg.in_gen (glbwit wit1) p) >>= fun p ->
       interp_genarg ist (Genarg.in_gen (glbwit wit2) q) >>= fun q ->
-      let p = Value.cast (topwit wit1) p in
-      let q = Value.cast (topwit wit2) q in
-      Ftactic.return (Val.Dyn (Val.Pair (val_tag wit1, val_tag wit2), (p, q)))
+      Ftactic.return (Val.Dyn (Val.typ_pair, (p, q)))
     | ExtraArg s ->
-      Geninterp.generic_interp ist (Genarg.in_gen (glbwit wit) x)
+      Geninterp.interp wit ist x
 
 (** returns [true] for genargs which have the same meaning
     independently of goals. *)
@@ -1587,7 +1573,7 @@ and interp_genarg_constr_list ist x =
   let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
   let lc = Genarg.out_gen (glbwit (wit_list wit_constr)) x in
   let (sigma,lc) = interp_constr_list ist env sigma lc in
-  let lc = Value.of_list (val_tag wit_constr) lc in
+  let lc = in_list (val_tag wit_constr) lc in
   Sigma.Unsafe.of_pair (Ftactic.return lc, sigma)
   end }
 
@@ -1597,7 +1583,8 @@ and interp_genarg_var_list ist x =
   let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
   let lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in
   let lc = interp_hyp_list ist env sigma lc in
-  Ftactic.return (Value.of_list (val_tag wit_var) lc)
+  let lc = in_list (val_tag wit_var) lc in
+  Ftactic.return lc
   end }
 
 (* Interprets tactic expressions : returns a "constr" *)
@@ -2055,6 +2042,13 @@ let hide_interp global t ot =
 (***************************************************************************)
 (** Register standard arguments *)
 
+let register_interp0 wit f =
+  let open Ftactic.Notations in
+  let interp ist v =
+    f ist v >>= fun v -> Ftactic.return (Val.inject (val_tag wit) v)
+  in
+  Geninterp.register_interp0 wit interp
+
 let def_intern ist x = (ist, x)
 let def_subst _ x = x
 let def_interp ist x = Ftactic.return x
@@ -2062,7 +2056,7 @@ let def_interp ist x = Ftactic.return x
 let declare_uniform t =
   Genintern.register_intern0 t def_intern;
   Genintern.register_subst0 t def_subst;
-  Geninterp.register_interp0 t def_interp
+  register_interp0 t def_interp
 
 let () =
   declare_uniform wit_unit
@@ -2103,33 +2097,31 @@ let interp_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigm
   }
 
 let () =
-  Geninterp.register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
-  Geninterp.register_interp0 wit_ref (lift interp_reference);
-  Geninterp.register_interp0 wit_ident (lift interp_ident);
-  Geninterp.register_interp0 wit_var (lift interp_hyp);
-  Geninterp.register_interp0 wit_intro_pattern (lifts interp_intro_pattern);
-  Geninterp.register_interp0 wit_clause_dft_concl (lift interp_clause);
-  Geninterp.register_interp0 wit_constr (lifts interp_constr);
-  Geninterp.register_interp0 wit_sort (lifts (fun _ _ evd s -> interp_sort evd s));
-  Geninterp.register_interp0 wit_tacvalue (fun ist v -> Ftactic.return v);
-  Geninterp.register_interp0 wit_red_expr (lifts interp_red_expr);
-  Geninterp.register_interp0 wit_quant_hyp (lift interp_declared_or_quantified_hypothesis);
-  Geninterp.register_interp0 wit_open_constr (lifts interp_open_constr);
-  Geninterp.register_interp0 wit_bindings interp_bindings';
-  Geninterp.register_interp0 wit_constr_with_bindings interp_constr_with_bindings';
-  Geninterp.register_interp0 wit_constr_may_eval (lifts interp_constr_may_eval);
+  register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
+  register_interp0 wit_ref (lift interp_reference);
+  register_interp0 wit_ident (lift interp_ident);
+  register_interp0 wit_var (lift interp_hyp);
+  register_interp0 wit_intro_pattern (lifts interp_intro_pattern);
+  register_interp0 wit_clause_dft_concl (lift interp_clause);
+  register_interp0 wit_constr (lifts interp_constr);
+  register_interp0 wit_tacvalue (fun ist v -> Ftactic.return v);
+  register_interp0 wit_red_expr (lifts interp_red_expr);
+  register_interp0 wit_quant_hyp (lift interp_declared_or_quantified_hypothesis);
+  register_interp0 wit_open_constr (lifts interp_open_constr);
+  register_interp0 wit_bindings interp_bindings';
+  register_interp0 wit_constr_with_bindings interp_constr_with_bindings';
   ()
 
 let () =
   let interp ist tac = Ftactic.return (Value.of_closure ist tac) in
-  Geninterp.register_interp0 wit_tactic interp
+  register_interp0 wit_tactic interp
 
 let () =
   let interp ist tac = interp_tactic ist tac >>= fun () -> Ftactic.return () in
-  Geninterp.register_interp0 wit_ltac interp
+  register_interp0 wit_ltac interp
 
 let () =
-  Geninterp.register_interp0 wit_uconstr (fun ist c -> Ftactic.nf_enter { enter = begin fun gl ->
+  register_interp0 wit_uconstr (fun ist c -> Ftactic.nf_enter { enter = begin fun gl ->
     Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) c)
   end })
 
diff --git a/ltac/tacinterp.mli b/ltac/tacinterp.mli
index 92f12fc8f7..8bb6ee4cdf 100644
--- a/ltac/tacinterp.mli
+++ b/ltac/tacinterp.mli
@@ -18,14 +18,14 @@ val ltac_trace_info : ltac_trace Exninfo.t
 
 module Value :
 sig
-  type t = Val.t
+  type t = Geninterp.Val.t
   val of_constr : constr -> t
   val to_constr : t -> constr option
   val of_int : int -> t
   val to_int : t -> int option
   val to_list : t -> t list option
   val of_closure : Geninterp.interp_sign -> glob_tactic_expr -> t
-  val cast : 'a typed_abstract_argument_type -> Val.t -> 'a
+  val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a
 end
 
 (** Values for interpretation *)
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index 438219f5a3..54d32f2666 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -301,7 +301,6 @@ let () =
   Genintern.register_subst0 wit_tactic subst_tactic;
   Genintern.register_subst0 wit_ltac subst_tactic;
   Genintern.register_subst0 wit_constr subst_glob_constr;
-  Genintern.register_subst0 wit_sort (fun _ v -> v);
   Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v);
   Genintern.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c);
   Genintern.register_subst0 wit_open_constr (fun subst c -> subst_glob_constr subst c);
@@ -309,5 +308,4 @@ let () =
   Genintern.register_subst0 wit_quant_hyp subst_declared_or_quantified_hypothesis;
   Genintern.register_subst0 wit_bindings subst_bindings;
   Genintern.register_subst0 wit_constr_with_bindings subst_glob_with_bindings;
-  Genintern.register_subst0 wit_constr_may_eval subst_raw_may_eval;
   ()
diff --git a/ltac/tauto.ml b/ltac/tauto.ml
index a86fdb98a9..7cda8d9147 100644
--- a/ltac/tauto.ml
+++ b/ltac/tauto.ml
@@ -11,6 +11,7 @@ open Hipattern
 open Names
 open Pp
 open Genarg
+open Geninterp
 open Stdarg
 open Misctypes
 open Tacexpr
@@ -54,12 +55,13 @@ type tauto_flags = {
   strict_unit : bool;
 }
 
-let wit_tauto_flags : tauto_flags uniform_genarg_type =
-  Genarg.create_arg "tauto_flags"
+let tag_tauto_flags : tauto_flags Val.typ = Val.create "tauto_flags"
 
-let assoc_flags ist =
-  let v = Id.Map.find (Names.Id.of_string "tauto_flags") ist.lfun in
-  try Value.cast (topwit wit_tauto_flags) v with _ -> assert false
+let assoc_flags ist : tauto_flags =
+  let Val.Dyn (tag, v) = Id.Map.find (Names.Id.of_string "tauto_flags") ist.lfun in
+  match Val.eq tag tag_tauto_flags with
+  | None -> assert false
+  | Some Refl -> v
 
 (* Whether inner not are unfolded *)
 let negation_unfolding = ref true
@@ -256,7 +258,7 @@ let tauto_power_flags = {
 let with_flags flags _ ist =
   let f = (loc, Id.of_string "f") in
   let x = (loc, Id.of_string "x") in
-  let arg = Val.Dyn (val_tag (topwit wit_tauto_flags), flags) in
+  let arg = Val.Dyn (tag_tauto_flags, flags) in
   let ist = { ist with lfun = Id.Map.add (snd x) arg ist.lfun } in
   eval_tactic_ist ist (TacArg (loc, TacCall (loc, ArgVar f, [Reference (ArgVar x)])))
 
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index e60b470fdf..53d2089c04 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -730,9 +730,7 @@ let () =
   Grammar.register0 wit_var (Prim.var);
   Grammar.register0 wit_ref (Prim.reference);
   Grammar.register0 wit_quant_hyp (Tactic.quantified_hypothesis);
-  Grammar.register0 wit_sort (Constr.sort);
   Grammar.register0 wit_constr (Constr.constr);
-  Grammar.register0 wit_constr_may_eval (Tactic.constr_may_eval);
   Grammar.register0 wit_uconstr (Tactic.uconstr);
   Grammar.register0 wit_open_constr (Tactic.open_constr);
   Grammar.register0 wit_constr_with_bindings (Tactic.constr_with_bindings);
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 9d78a51ef6..29ecb94ca8 100644
--- a/plugins/decl_mode/decl_expr.mli
+++ b/plugins/decl_mode/decl_expr.mli
@@ -99,4 +99,4 @@ type proof_instr =
     (Term.constr statement,
      Term.constr,
      proof_pattern,
-     Genarg.Val.t) gen_proof_instr
+     Geninterp.Val.t) gen_proof_instr
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 587d10d1cc..b04c4a50c9 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -122,6 +122,7 @@ let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma
 let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
 
 ARGUMENT EXTEND firstorder_using
+  TYPED AS reference_list
   PRINTED BY pr_firstorder_using_typed
   RAW_TYPED AS reference_list
   RAW_PRINTED BY pr_firstorder_using_raw
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index e93c395e3d..0ba18f568a 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -65,6 +65,7 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
 
 
 ARGUMENT EXTEND fun_ind_using
+  TYPED AS constr_with_bindings option
   PRINTED BY pr_fun_ind_using_typed
   RAW_TYPED AS constr_with_bindings_opt
   RAW_PRINTED BY pr_fun_ind_using
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index a15b0eb05a..e4c8da93b1 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -24,7 +24,7 @@ let loc = Loc.ghost
 let cont = Id.of_string "cont"
 let x = Id.of_string "x"
 
-let make_cont (k : Genarg.Val.t) (c : Constr.t) =
+let make_cont (k : Val.t) (c : Constr.t) =
   let c = Tacinterp.Value.of_constr c in
   let tac = TacCall (loc, ArgVar (loc, cont), [Reference (ArgVar (loc, x))]) in
   let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index 07a1ae833b..ca6aba9a0f 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -45,7 +45,7 @@ val ic : constr_expr -> Evd.evar_map * constr
 val from_name : ring_info Spmap.t ref
 
 val ring_lookup :
-  Genarg.Val.t ->
+  Geninterp.Val.t ->
   constr list ->
   constr list -> constr -> unit Proofview.tactic
 
@@ -73,6 +73,6 @@ val add_field_theory :
 val field_from_name : field_info Spmap.t ref
 
 val field_lookup :
-  Genarg.Val.t ->
+  Geninterp.Val.t ->
   constr list ->
   constr list -> constr -> unit Proofview.tactic
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5e6a3eac73..21eb100b4e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -49,7 +49,7 @@ open Context.Named.Declaration
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 type var_map = constr_under_binders Id.Map.t
 type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t
-type unbound_ltac_var_map = Genarg.Val.t Id.Map.t
+type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t
 type ltac_var_map = {
   ltac_constrs : var_map;
   ltac_uconstrs : uconstr_var_map;
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 91320f20a5..824bb11aa4 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -29,7 +29,7 @@ type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 
 type var_map = Pattern.constr_under_binders Id.Map.t
 type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t
-type unbound_ltac_var_map = Genarg.Val.t Id.Map.t
+type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t
 
 type ltac_var_map = {
   ltac_constrs : var_map;
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 7949bafcbb..9ab6895f3b 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -14,6 +14,7 @@ open Util
 open Constrexpr
 open Tacexpr
 open Genarg
+open Geninterp
 open Constrarg
 open Libnames
 open Ppextend
@@ -97,23 +98,38 @@ module Make
   let keyword x = tag_keyword (str x)
   let primitive x = tag_primitive (str x)
 
-  let rec pr_value lev (Val.Dyn (tag, x)) : std_ppcmds = match tag with
-  | Val.List tag ->
-    pr_sequence (fun x -> pr_value lev (Val.Dyn (tag, x))) x
-  | Val.Opt tag -> pr_opt_no_spc (fun x -> pr_value lev (Val.Dyn (tag, x))) x
-  | Val.Pair (tag1, tag2) ->
-    str "(" ++ pr_value lev (Val.Dyn (tag1, fst x)) ++ str ", " ++
-      pr_value lev (Val.Dyn (tag1, fst x)) ++ str ")"
-  | Val.Base t ->
-    let name = Val.repr t in
-    let default = str "<" ++ str name ++ str ">" in
-    match ArgT.name name with
-    | None -> default
-    | Some (ArgT.Any arg) ->
-      let wit = ExtraArg arg in
-      match Val.eq (val_tag (Topwit wit)) (Val.Base t) with
+  let has_type (Val.Dyn (tag, x)) t = match Val.eq tag t with
+  | None -> false
+  | Some _ -> true
+
+  let unbox : type a. Val.t -> a Val.typ -> a= fun (Val.Dyn (tag, x)) t ->
+  match Val.eq tag t with
+  | None -> assert false
+  | Some Refl -> x
+
+  let rec pr_value lev v : std_ppcmds =
+    if has_type v Val.typ_list then
+      pr_sequence (fun x -> pr_value lev x) (unbox v Val.typ_list)
+    else if has_type v Val.typ_opt then
+      pr_opt_no_spc (fun x -> pr_value lev x) (unbox v Val.typ_opt)
+    else if has_type v Val.typ_pair then
+      let (v1, v2) = unbox v Val.typ_pair in
+      str "(" ++ pr_value lev v1 ++ str ", " ++ pr_value lev v2 ++ str ")"
+    else
+      let Val.Dyn (tag, x) = v in
+      let name = Val.repr tag in
+      let default = str "<" ++ str name ++ str ">" in
+      match ArgT.name name with
       | None -> default
-      | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x)
+      | Some (ArgT.Any arg) ->
+        let wit = ExtraArg arg in
+        match val_tag (Topwit wit) with
+        | Val.Base t ->
+          begin match Val.eq t tag with
+          | None -> default
+          | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x)
+          end
+        | _ -> default
 
   let pr_with_occurrences pr (occs,c) =
     match occs with
@@ -1349,8 +1365,6 @@ let () =
     (pr_clauses (Some true) pr_lident)
     (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id)))
   ;
-  Genprint.register_print0 Constrarg.wit_sort
-    pr_glob_sort pr_glob_sort (pr_sort Evd.empty);
   Genprint.register_print0
     Constrarg.wit_constr
     Ppconstr.pr_constr_expr
@@ -1378,11 +1392,6 @@ let () =
     (pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
     (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
     (fun it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it)));
-  Genprint.register_print0 Constrarg.wit_constr_may_eval
-    (pr_may_eval pr_constr_expr pr_lconstr_expr (pr_or_by_notation pr_reference) pr_constr_pattern_expr)
-    (pr_may_eval (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)
-      (pr_or_var (pr_and_short_name pr_evaluable_reference)) (pr_pat_and_constr_expr pr_glob_constr))
-    pr_constr;
   Genprint.register_print0 Constrarg.wit_constr_with_bindings
     (pr_with_bindings pr_constr_expr pr_lconstr_expr)
     (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 1608cae751..b1e650b872 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -11,6 +11,7 @@
 
 open Pp
 open Genarg
+open Geninterp
 open Names
 open Constrexpr
 open Tacexpr
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index d4858bac4f..d49bef1fd2 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -8,6 +8,7 @@
 
 open Pp
 open Genarg
+open Geninterp
 open Tacexpr
 open Ppextend
 open Environ
diff --git a/tactics/auto.ml b/tactics/auto.ml
index fc6ff03b4b..6b58baa997 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -156,11 +156,16 @@ let conclPattern concl pat tac =
        constr_bindings env sigma >>= fun constr_bindings ->
      let open Genarg in
      let open Geninterp in
-     let inj c = Val.Dyn (val_tag (topwit Constrarg.wit_constr), c) in
+     let inj c = match val_tag (topwit Constrarg.wit_constr) with
+     | Val.Base tag -> Val.Dyn (tag, c)
+     | _ -> assert false
+     in
      let fold id c accu = Id.Map.add id (inj c) accu in
      let lfun = Id.Map.fold fold constr_bindings Id.Map.empty in
      let ist = { lfun; extra = TacStore.empty } in
-     Ftactic.run (Geninterp.generic_interp ist tac) (fun _ -> Proofview.tclUNIT ())
+     match tac with
+     | GenArg (Glbwit wit, tac) ->
+      Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ())
   end }
 
 (***********************************************************)
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 4816f8a452..950eeef520 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -106,9 +106,9 @@ let one_base general_rewrite_maybe_in tac_main bas =
   let lrul = List.map (fun h -> 
   let tac = match h.rew_tac with
   | None -> Proofview.tclUNIT ()
-  | Some tac ->
+  | Some (Genarg.GenArg (Genarg.Glbwit wit, tac)) ->
     let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in
-    Ftactic.run (Geninterp.generic_interp ist tac) (fun _ -> Proofview.tclUNIT ())
+    Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ())
   in
     (h.rew_ctx,h.rew_lemma,h.rew_l2r,tac)) lrul in
     Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac (ctx,csr,dir,tc) ->
diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml
deleted file mode 100644
index 0080758000..0000000000
--- a/tactics/geninterp.ml
+++ /dev/null
@@ -1,35 +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        *)
-(************************************************************************)
-
-open Names
-open Genarg
-
-module TacStore = Store.Make(struct end)
-
-type interp_sign = {
-  lfun : Val.t Id.Map.t;
-  extra : TacStore.t }
-
-type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
-
-module InterpObj =
-struct
-  type ('raw, 'glb, 'top) obj = ('glb, 'top) interp_fun
-  let name = "interp"
-  let default _ = None
-end
-
-module Interp = Register(InterpObj)
-
-let interp = Interp.obj
-let register_interp0 = Interp.register0
-
-let generic_interp ist (GenArg (Glbwit wit, v)) =
-  let open Ftactic.Notations in
-  interp wit ist v >>= fun ans ->
-  Ftactic.return (Val.Dyn (val_tag (topwit wit), ans))
diff --git a/tactics/geninterp.mli b/tactics/geninterp.mli
deleted file mode 100644
index 0992db7a29..0000000000
--- a/tactics/geninterp.mli
+++ /dev/null
@@ -1,27 +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        *)
-(************************************************************************)
-
-(** Interpretation functions for generic arguments. *)
-
-open Names
-open Genarg
-
-module TacStore : Store.S
-
-type interp_sign = {
-  lfun : Val.t Id.Map.t;
-  extra : TacStore.t }
-
-type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
-
-val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun
-
-val generic_interp : (glob_generic_argument, Val.t) interp_fun
-
-val register_interp0 :
-  ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 358f6d6468..d53c1cc04a 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -14,15 +14,25 @@ open Misctypes
 open Genarg
 open Stdarg
 open Constrarg
+open Geninterp
 
 exception CannotCoerceTo of string
 
 let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) =
-  Genarg.create_arg "constr_context"
+  let wit = Genarg.create_arg "constr_context" in
+  let () = register_val0 wit None in
+  wit
 
 (* includes idents known to be bound and references *)
 let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) =
-  Genarg.create_arg "constr_under_binders"
+  let wit = Genarg.create_arg "constr_under_binders" in
+  let () = register_val0 wit None in
+  wit
+
+(** All the types considered here are base types *)
+let val_tag wit = match val_tag wit with
+| Val.Base t -> t
+| _ -> assert false
 
 let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
   let Val.Dyn (t, _) = v in
@@ -30,7 +40,7 @@ let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v w
   | None -> false
   | Some Refl -> true
 
-let prj : type a. a Val.tag -> Val.t -> a option = fun t v ->
+let prj : type a. a Val.typ -> Val.t -> a option = fun t v ->
   let Val.Dyn (t', x) = v in
   match Val.eq t t' with
   | None -> None
@@ -74,23 +84,11 @@ let to_int v =
     Some (out_gen (topwit wit_int) v)
   else None
 
-let to_list v =
-  let v = normalize v in
-  let Val.Dyn (tag, v) = v in
-  match tag with
-  | Val.List t -> Some (List.map (fun x -> Val.Dyn (t, x)) v)
-  | _ -> None
-
-let of_list t v = Val.Dyn (Val.List t, v)
+let to_list v = prj Val.typ_list v
 
-let to_option v =
-  let v = normalize v in
-  let Val.Dyn (tag, v) = v in
-  match tag with
-  | Val.Opt t -> Some (Option.map (fun x -> Val.Dyn (t, x)) v)
-  | _ -> None
+let to_option v = prj Val.typ_opt v
 
-let of_option t v = Val.Dyn (Val.Opt t, v)
+let to_pair v = prj Val.typ_pair v
 
 end
 
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
index 87137fd2e7..7a963f95f3 100644
--- a/tactics/taccoerce.mli
+++ b/tactics/taccoerce.mli
@@ -12,6 +12,7 @@ open Term
 open Misctypes
 open Pattern
 open Genarg
+open Geninterp
 
 (** Coercions from highest level generic arguments to actual data used by Ltac
     interpretation. Those functions examinate dynamic types and try to return
@@ -41,9 +42,8 @@ sig
   val of_int : int -> t
   val to_int : t -> int option
   val to_list : t -> t list option
-  val of_list : 'a Val.tag -> 'a list -> t
   val to_option : t -> t option option
-  val of_option : 'a Val.tag -> 'a option -> t
+  val to_pair : t -> (t * t) option
 end
 
 (** {5 Coercion functions} *)
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index ab8069225d..48722f655a 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,5 +1,3 @@
-Ftactic
-Geninterp
 Dnet
 Dn
 Btermdn