aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--dev/printers.mllib2
-rw-r--r--dev/top_printers.ml4
-rw-r--r--engine/geninterp.ml67
-rw-r--r--engine/geninterp.mli42
-rw-r--r--grammar/argextend.ml412
-rw-r--r--interp/constrarg.ml42
-rw-r--r--interp/constrarg.mli2
-rw-r--r--interp/stdarg.ml6
-rw-r--r--lib/genarg.ml58
-rw-r--r--lib/genarg.mli38
-rw-r--r--ltac/extraargs.mli2
-rw-r--r--ltac/extratactics.ml44
-rw-r--r--ltac/tacenv.ml3
-rw-r--r--ltac/tacenv.mli1
-rw-r--r--ltac/tacinterp.ml5
-rw-r--r--ltac/tacinterp.mli4
-rw-r--r--ltac/tauto.ml5
-rw-r--r--plugins/decl_mode/decl_expr.mli2
-rw-r--r--plugins/quote/g_quote.ml42
-rw-r--r--plugins/setoid_ring/newring.mli4
-rw-r--r--pretyping/pretyping.ml2
-rw-r--r--pretyping/pretyping.mli2
-rw-r--r--printing/pptactic.ml1
-rw-r--r--printing/pptactic.mli1
-rw-r--r--printing/pptacticsig.mli1
-rw-r--r--tactics/taccoerce.ml9
-rw-r--r--tactics/taccoerce.mli1
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