27 files changed, 186 insertions, 136 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 9f25ba55e..5d10f54fb 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 29ea08e02..f9c1971a8 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/geninterp.ml b/engine/geninterp.ml
index be4011cb6..9e866f0cf 100644
--- a/engine/geninterp.ml
+++ b/engine/geninterp.ml
@@ -11,6 +11,73 @@ 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 list_tag = ValT.create "list"
+  let opt_tag = ValT.create "option"
+  let pair_tag = 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 (list_tag, List.map (fun x -> inject tag x) x)
+  | Opt tag -> Dyn (opt_tag, Option.map (fun x -> inject tag x) x)
+  | Pair (tag1, tag2) ->
+    Dyn (pair_tag, (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 }
diff --git a/engine/geninterp.mli b/engine/geninterp.mli
index 0e7ed1847..3c87b2512 100644
--- a/engine/geninterp.mli
+++ b/engine/geninterp.mli
@@ -11,6 +11,48 @@
 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 list_tag : t list typ
+  val opt_tag : t option typ
+  val pair_tag : (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 = {
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index dca3e1656..2618e5d89 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
@@ -147,20 +148,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 46be0b8a1..99f0a2da6 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,50 @@ 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"
+  make0 ~dyn:(val_tag (topwit wit_ident)) "var"
 
-let wit_ref = Genarg.make0 "ref"
+let wit_ref = make0 "ref"
 
-let wit_quant_hyp = Genarg.make0 "quant_hyp"
+let wit_quant_hyp = make0 "quant_hyp"
 
 let wit_sort : (glob_sort, glob_sort, sorts) genarg_type =
-  Genarg.make0 "sort"
+  make0 "sort"
 
 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 d38b1183c..6407b61af 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -69,7 +69,7 @@ val wit_red_expr :
   (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 244cdd0a7..9e85dbaf3 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"
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 3ff9afa60..69408fb1a 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,37 +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 typ * 'a -> t
-
-  let eq = ValT.eq
-  let repr = ValT.repr
-
-  let rec pr : type a. a typ -> std_ppcmds = fun t -> str (repr t)
-
-  let list_tag = ValT.create "list"
-  let opt_tag = ValT.create "option"
-  let pair_tag = 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 (list_tag, List.map (fun x -> inject tag x) x)
-  | Opt tag -> Dyn (opt_tag, Option.map (fun x -> inject tag x) x)
-  | Pair (tag1, tag2) ->
-    Dyn (pair_tag, (inject tag1 (fst x), inject tag2 (snd x)))
-
-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
@@ -187,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 04113ae28..b8bb6af04 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -86,42 +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 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 list_tag : t list typ
-  val opt_tag : t option typ
-  val pair_tag : (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. *)
-
 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} *)
@@ -186,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 14aa69875..4d1d8ba7f 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 0b475340e..eda530c26 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)
@@ -939,8 +939,10 @@ type 'i test =
   | Test of cmp * 'i * 'i
 
 let wit_cmp : (cmp,cmp,cmp) Genarg.genarg_type = Genarg.make0 "cmp"
+let _ = Geninterp.register_val0 wit_cmp None
 let wit_test : (int or_var test,int or_var test,int test) Genarg.genarg_type =
   Genarg.make0 "tactest"
+let _ = Geninterp.register_val0 wit_test None
 
 let pr_cmp = function
   | Eq -> Pp.str"="
diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml
index d2d3f3117..f2dbb5b6c 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 88b54993b..94e14223a 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/tacinterp.ml b/ltac/tacinterp.ml
index 6e76b1910..f39a42271 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
@@ -118,7 +119,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
diff --git a/ltac/tacinterp.mli b/ltac/tacinterp.mli
index 92f12fc8f..8bb6ee4cd 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/tauto.ml b/ltac/tauto.ml
index b0958b394..c075d05bb 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
@@ -55,7 +56,9 @@ type tauto_flags = {
 }
 
 let wit_tauto_flags : tauto_flags uniform_genarg_type =
-  Genarg.create_arg "tauto_flags"
+  let wit = Genarg.create_arg "tauto_flags" in
+  let () = register_val0 wit None in
+  wit
 
 let assoc_flags ist =
   let v = Id.Map.find (Names.Id.of_string "tauto_flags") ist.lfun in
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 9d78a51ef..29ecb94ca 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/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index a15b0eb05..e4c8da93b 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 07a1ae833..ca6aba9a0 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 5e6a3eac7..21eb100b4 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 91320f20a..824bb11aa 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 018e29cd2..a15fa772f 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
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 1608cae75..b1e650b87 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 d4858bac4..d49bef1fd 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/taccoerce.ml b/tactics/taccoerce.ml
index 298257e45..a03c529cc 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -14,15 +14,20 @@ 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
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
index 75a3b347d..82e1910f7 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