Rolling our own dynamic types for Ltac2.

This prevents careless confusions with generic arguments from Coq.

10 files changed, 49 insertions, 30 deletions

diff --git a/_CoqProject b/_CoqProject
index ffe1dda032..fc9df4ee3f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -2,6 +2,8 @@
 -I src/
 -bypass-API
 
+src/tac2dyn.ml
+src/tac2dyn.mli
 src/tac2expr.mli
 src/tac2env.ml
 src/tac2env.mli
diff --git a/src/ltac2_plugin.mlpack b/src/ltac2_plugin.mlpack
index f9fa2fafd8..92f391a085 100644
--- a/src/ltac2_plugin.mlpack
+++ b/src/ltac2_plugin.mlpack
@@ -1,3 +1,4 @@
+Tac2dyn
 Tac2env
 Tac2print
 Tac2intern
diff --git a/src/tac2core.ml b/src/tac2core.ml
index d14849a2a6..e865c1378f 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -10,8 +10,8 @@ open CSig
 open Pp
 open Names
 open Genarg
-open Geninterp
 open Tac2env
+open Tac2dyn
 open Tac2expr
 open Tac2interp
 open Tac2entries.Pltac
@@ -70,8 +70,8 @@ let of_rec_declaration (nas, ts, cs) =
   Value.of_array Value.of_constr ts,
   Value.of_array Value.of_constr cs)
 
-let val_valexpr : valexpr Val.typ = Val.create "ltac2:valexpr"
-let val_free : Id.Set.t Val.typ = Val.create "ltac2:free"
+let val_valexpr : valexpr Val.tag = Val.create "ltac2:valexpr"
+let val_free : Id.Set.t Val.tag = Val.create "ltac2:free"
 
 (** Stdlib exceptions *)
 
diff --git a/src/tac2dyn.ml b/src/tac2dyn.ml
new file mode 100644
index 0000000000..3f4fbca712
--- /dev/null
+++ b/src/tac2dyn.ml
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+module Val = Dyn.Make(struct end)
diff --git a/src/tac2dyn.mli b/src/tac2dyn.mli
new file mode 100644
index 0000000000..e4b18ba373
--- /dev/null
+++ b/src/tac2dyn.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** Dynamic arguments for Ltac2. *)
+
+module Val : Dyn.S
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 42203a32e5..0b02ba2656 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -185,7 +185,7 @@ type valexpr =
   (** Closures *)
 | ValOpn of KerName.t * valexpr array
   (** Open constructors *)
-| ValExt : 'a Geninterp.Val.typ * 'a -> valexpr
+| ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
   (** Arbitrary data *)
 
 and closure = {
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index a9a0f5a479..61b6d56b6c 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -9,18 +9,14 @@
 open Util
 open Globnames
 open Genarg
-open Geninterp
+open Tac2dyn
 open Tac2expr
 open Tac2interp
 
 (** Dynamic tags *)
 
-let val_tag t = match val_tag t with
-| Val.Base t -> t
-| _ -> assert false
-
-let val_constr = val_tag (topwit Stdarg.wit_constr)
-let val_ident = val_tag (topwit Stdarg.wit_ident)
+let val_constr = Val.create "ltac2:constr"
+let val_ident = Val.create "ltac2:ident"
 let val_pattern = Val.create "ltac2:pattern"
 let val_pp = Val.create "ltac2:pp"
 let val_sort = Val.create "ltac2:sort"
@@ -30,10 +26,10 @@ let val_constant = Val.create "ltac2:constant"
 let val_constructor = Val.create "ltac2:constructor"
 let val_projection = Val.create "ltac2:projection"
 let val_univ = Val.create "ltac2:universe"
-let val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.typ =
+let val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.tag =
   Val.create "ltac2:kont"
 
-let extract_val (type a) (type b) (tag : a Val.typ) (tag' : b Val.typ) (v : b) : a =
+let extract_val (type a) (type b) (tag : a Val.tag) (tag' : b Val.tag) (v : b) : a =
 match Val.eq tag tag' with
 | None -> assert false
 | Some Refl -> v
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index 71d90ba940..1ce163256d 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Geninterp
 open Names
 open EConstr
+open Tac2dyn
 open Tac2expr
 
 (** {5 Ltac2 FFI} *)
@@ -65,20 +65,20 @@ val to_constant : valexpr -> Constant.t
 val of_reference : Globnames.global_reference -> valexpr
 val to_reference : valexpr -> Globnames.global_reference
 
-val of_ext : 'a Val.typ -> 'a -> valexpr
-val to_ext : 'a Val.typ -> valexpr -> 'a
+val of_ext : 'a Val.tag -> 'a -> valexpr
+val to_ext : 'a Val.tag -> valexpr -> 'a
 
 (** {5 Dynamic tags} *)
 
-val val_constr : EConstr.t Val.typ
-val val_ident : Id.t Val.typ
-val val_pattern : Pattern.constr_pattern Val.typ
-val val_pp : Pp.t Val.typ
-val val_sort : ESorts.t Val.typ
-val val_cast : Constr.cast_kind Val.typ
-val val_inductive : inductive Val.typ
-val val_constant : Constant.t Val.typ
-val val_constructor : constructor Val.typ
-val val_projection : Projection.t Val.typ
-val val_univ : Univ.universe_level Val.typ
-val val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.typ
+val val_constr : EConstr.t Val.tag
+val val_ident : Id.t Val.tag
+val val_pattern : Pattern.constr_pattern Val.tag
+val val_pp : Pp.t Val.tag
+val val_sort : ESorts.t Val.tag
+val val_cast : Constr.cast_kind Val.tag
+val val_inductive : inductive Val.tag
+val val_constant : Constant.t Val.tag
+val val_constructor : constructor Val.tag
+val val_projection : Projection.t Val.tag
+val val_univ : Univ.universe_level Val.tag
+val val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.tag
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index 691c795502..3be95ac828 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -23,7 +23,7 @@ let () = register_handler begin function
 | _ -> raise Unhandled
 end
 
-let val_exn = Geninterp.Val.create "ltac2:exn"
+let val_exn = Tac2dyn.Val.create "ltac2:exn"
 
 type environment = valexpr Id.Map.t
 
diff --git a/src/tac2interp.mli b/src/tac2interp.mli
index f99008c506..18522c3c91 100644
--- a/src/tac2interp.mli
+++ b/src/tac2interp.mli
@@ -27,6 +27,6 @@ val set_env : environment -> Glob_term.unbound_ltac_var_map -> Glob_term.unbound
 exception LtacError of KerName.t * valexpr array
 (** Ltac2-defined exceptions seen from OCaml side *)
 
-val val_exn : Exninfo.iexn Geninterp.Val.typ
+val val_exn : Exninfo.iexn Tac2dyn.Val.tag
 (** Toplevel representation of OCaml exceptions. Invariant: no [LtacError]
     should be put into a value with tag [val_exn]. *)