Moving valexpr definition to Tac2ffi.

12 files changed, 70 insertions, 28 deletions

diff --git a/src/ltac2_plugin.mlpack b/src/ltac2_plugin.mlpack
index 70f97b9d1e..a2237f4d26 100644
--- a/src/ltac2_plugin.mlpack
+++ b/src/ltac2_plugin.mlpack
@@ -1,6 +1,6 @@
 Tac2dyn
-Tac2env
 Tac2ffi
+Tac2env
 Tac2print
 Tac2intern
 Tac2interp
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index d622aaba69..78fe7b5bd9 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -773,7 +773,7 @@ let pr_frame = function
 let () = register_handler begin function
 | Tac2interp.LtacError (kn, args) ->
   let t_exn = KerName.make2 Tac2env.coq_prefix (Label.make "exn") in
-  let v = ValOpn (kn, args) in
+  let v = Tac2ffi.ValOpn (kn, args) in
   let t = GTypRef (Other t_exn, []) in
   let c = Tac2print.pr_valexpr (Global.env ()) Evd.empty v t in
   hov 0 (str "Uncaught Ltac2 exception:" ++ spc () ++ hov 0 c)
diff --git a/src/tac2env.ml b/src/tac2env.ml
index 831c6a3b42..0aa2da77ae 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -12,6 +12,7 @@ open Names
 open Libnames
 open Tac2dyn
 open Tac2expr
+open Tac2ffi
 
 type global_data = {
   gdata_expr : glb_tacexpr;
@@ -237,6 +238,10 @@ type 'a or_glb_tacexpr =
 | GlbVal of 'a
 | GlbTacexpr of glb_tacexpr
 
+type environment = {
+  env_ist : valexpr Id.Map.t;
+}
+
 type ('a, 'b, 'r) intern_fun = Genintern.glob_sign -> 'a -> 'b * 'r glb_typexpr
 
 type ('a, 'b) ml_object = {
diff --git a/src/tac2env.mli b/src/tac2env.mli
index 89e22f07d5..85dba90262 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -12,6 +12,7 @@ open Libnames
 open Nametab
 open Tac2dyn
 open Tac2expr
+open Tac2ffi
 
 (** Ltac2 global environment *)
 
@@ -111,6 +112,10 @@ type 'a or_glb_tacexpr =
 
 type ('a, 'b, 'r) intern_fun = Genintern.glob_sign -> 'a -> 'b * 'r glb_typexpr
 
+type environment = {
+  env_ist : valexpr Id.Map.t;
+}
+
 type ('a, 'b) ml_object = {
   ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b or_glb_tacexpr, 'r) intern_fun;
   ml_subst : Mod_subst.substitution -> 'b -> 'b;
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index bbe127e94d..c787870c65 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -187,27 +187,3 @@ type frame =
 | FrExtn : ('a, 'b) Tac2dyn.Arg.tag * 'b -> frame
 
 type backtrace = frame list
-
-type ('a, _) arity =
-| OneAty : ('a, 'a -> 'a Proofview.tactic) arity
-| AddAty : ('a, 'b) arity -> ('a, 'a -> 'b) arity
-
-type valexpr =
-| ValInt of int
-  (** Immediate integers *)
-| ValBlk of tag * valexpr array
-  (** Structured blocks *)
-| ValStr of Bytes.t
-  (** Strings *)
-| ValCls of ml_tactic
-  (** Closures *)
-| ValOpn of KerName.t * valexpr array
-  (** Open constructors *)
-| ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
-  (** Arbitrary data *)
-
-and ml_tactic = MLTactic : (valexpr, 'v) arity * 'v -> ml_tactic
-
-type environment = {
-  env_ist : valexpr Id.Map.t;
-}
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index b4191acd60..3e9842b926 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -14,6 +14,26 @@ open Tac2dyn
 open Tac2expr
 open Proofview.Notations
 
+type ('a, _) arity =
+| OneAty : ('a, 'a -> 'a Proofview.tactic) arity
+| AddAty : ('a, 'b) arity -> ('a, 'a -> 'b) arity
+
+type valexpr =
+| ValInt of int
+  (** Immediate integers *)
+| ValBlk of tag * valexpr array
+  (** Structured blocks *)
+| ValStr of Bytes.t
+  (** Strings *)
+| ValCls of ml_tactic
+  (** Closures *)
+| ValOpn of KerName.t * valexpr array
+  (** Open constructors *)
+| ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
+  (** Arbitrary data *)
+
+and ml_tactic = MLTactic : (valexpr, 'v) arity * 'v -> ml_tactic
+
 type 'a repr = {
   r_of : 'a -> valexpr;
   r_to : valexpr -> 'a;
@@ -166,7 +186,10 @@ let pattern = repr_ext val_pattern
 
 let internal_err =
   let open Names in
-  KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string "Internal"))
+  let coq_prefix =
+    MPfile (DirPath.make (List.map Id.of_string ["Init"; "Ltac2"]))
+  in
+  KerName.make2 coq_prefix (Label.of_id (Id.of_string "Internal"))
 
 (** FIXME: handle backtrace in Ltac2 exceptions *)
 let of_exn c = match fst c with
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index 489531671c..26e309e5fd 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -11,6 +11,28 @@ open EConstr
 open Tac2dyn
 open Tac2expr
 
+(** {5 Toplevel values} *)
+
+type ('a, _) arity =
+| OneAty : ('a, 'a -> 'a Proofview.tactic) arity
+| AddAty : ('a, 'b) arity -> ('a, 'a -> 'b) arity
+
+type valexpr =
+| ValInt of int
+  (** Immediate integers *)
+| ValBlk of tag * valexpr array
+  (** Structured blocks *)
+| ValStr of Bytes.t
+  (** Strings *)
+| ValCls of ml_tactic
+  (** Closures *)
+| ValOpn of KerName.t * valexpr array
+  (** Open constructors *)
+| ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
+  (** Arbitrary data *)
+
+and ml_tactic = MLTactic : (valexpr, 'v) arity * 'v -> ml_tactic
+
 (** {5 Ltac2 FFI} *)
 
 type 'a repr = {
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index 815fdffe0f..58a3a9a4ec 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -13,6 +13,7 @@ open Genarg
 open Names
 open Proofview.Notations
 open Tac2expr
+open Tac2ffi
 
 exception LtacError = Tac2ffi.LtacError
 
@@ -42,6 +43,10 @@ let with_frame frame tac =
     Proofview.tclUNIT ans
   else tac
 
+type environment = Tac2env.environment = {
+  env_ist : valexpr Id.Map.t;
+}
+
 let empty_environment = {
   env_ist = Id.Map.empty;
 }
diff --git a/src/tac2interp.mli b/src/tac2interp.mli
index 3acca72367..211ac95196 100644
--- a/src/tac2interp.mli
+++ b/src/tac2interp.mli
@@ -8,6 +8,9 @@
 
 open Names
 open Tac2expr
+open Tac2ffi
+
+type environment = Tac2env.environment
 
 val empty_environment : environment
 
diff --git a/src/tac2print.ml b/src/tac2print.ml
index 7113b01610..d39051c93e 100644
--- a/src/tac2print.ml
+++ b/src/tac2print.ml
@@ -12,6 +12,7 @@ open Genarg
 open Names
 open Tac2expr
 open Tac2env
+open Tac2ffi
 
 (** Utils *)
 
@@ -106,7 +107,7 @@ type exp_level = Tac2expr.exp_level =
 | E0
 
 let pr_atom = function
-| AtmInt n -> int n
+| AtmInt n -> Pp.int n
 | AtmStr s -> qstring s
 
 let pr_name = function
diff --git a/src/tac2print.mli b/src/tac2print.mli
index 01abd1efb1..9b9db2937d 100644
--- a/src/tac2print.mli
+++ b/src/tac2print.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Tac2expr
+open Tac2ffi
 
 (** {5 Printing types} *)
 
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 6512510f0a..6b3b997232 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -12,6 +12,7 @@ open Globnames
 open Misctypes
 open Genredexpr
 open Tac2expr
+open Tac2ffi
 open Proofview.Notations
 
 module Value = Tac2ffi