Moving Tac2ffi before Tac2interp.

4 files changed, 14 insertions, 4 deletions

diff --git a/src/ltac2_plugin.mlpack b/src/ltac2_plugin.mlpack
index 92f391a085..00ba5bc58e 100644
--- a/src/ltac2_plugin.mlpack
+++ b/src/ltac2_plugin.mlpack
@@ -2,9 +2,9 @@ Tac2dyn
 Tac2env
 Tac2print
 Tac2intern
+Tac2ffi
 Tac2interp
 Tac2entries
-Tac2ffi
 Tac2quote
 Tac2core
 Tac2tactics
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index 6a60562d1a..a0c51783ed 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Util
+open Names
 open Globnames
 open Genarg
 open Tac2dyn
@@ -42,6 +43,10 @@ match Val.eq tag tag' with
 | None -> assert false
 | Some Refl -> v
 
+(** Exception *)
+
+exception LtacError of KerName.t * valexpr array * backtrace
+
 (** Conversion functions *)
 
 let of_unit () = ValInt 0
@@ -148,7 +153,7 @@ let internal_err =
 
 (** FIXME: handle backtrace in Ltac2 exceptions *)
 let of_exn c = match fst c with
-| Tac2interp.LtacError (kn, c, _) -> ValOpn (kn, c)
+| LtacError (kn, c, _) -> ValOpn (kn, c)
 | _ -> ValOpn (internal_err, [|of_ext val_exn c|])
 
 let to_exn c = match c with
@@ -156,7 +161,7 @@ let to_exn c = match c with
   if Names.KerName.equal kn internal_err then
     to_ext val_exn c.(0)
   else
-    (Tac2interp.LtacError (kn, c, []), Exninfo.null)
+    (LtacError (kn, c, []), Exninfo.null)
 | _ -> assert false
 
 let exn = {
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index db3087534b..2282d34b3a 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -111,3 +111,8 @@ val val_free : Id.Set.t Val.tag
 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]. *)
+
+(** Exception *)
+
+exception LtacError of KerName.t * valexpr array * backtrace
+(** Ltac2-defined exceptions seen from OCaml side *)
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index b58ce6b851..e79ce87268 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -14,7 +14,7 @@ open Names
 open Proofview.Notations
 open Tac2expr
 
-exception LtacError of KerName.t * valexpr array * backtrace
+exception LtacError = Tac2ffi.LtacError
 
 let empty_environment = {
   env_ist = Id.Map.empty;