Moving the Val module to Geninterp.

7 files changed, 17 insertions, 7 deletions

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..eda530c265 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 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/tacinterp.ml b/ltac/tacinterp.ml
index 6e76b19106..f39a42271b 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 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/tauto.ml b/ltac/tauto.ml
index b0958b3948..c075d05bbf 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