4 files changed, 18 insertions, 19 deletions
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index 6fc3b2e0f2..4d84da14ce 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -15,20 +15,21 @@ open Tac2interp
 
 (** Dynamic tags *)
 
-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"
-let val_cast = Val.create "ltac2:cast"
-let val_inductive = Val.create "ltac2:inductive"
-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_exn = Val.create "exn"
+let val_constr = Val.create "constr"
+let val_ident = Val.create "ident"
+let val_pattern = Val.create "pattern"
+let val_pp = Val.create "pp"
+let val_sort = Val.create "sort"
+let val_cast = Val.create "cast"
+let val_inductive = Val.create "inductive"
+let val_constant = Val.create "constant"
+let val_constructor = Val.create "constructor"
+let val_projection = Val.create "projection"
+let val_univ = Val.create "universe"
 let val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.tag =
-  Val.create "ltac2:kont"
-let val_free : Names.Id.Set.t Val.tag = Val.create "ltac2:free"
+  Val.create "kont"
+let val_free : Names.Id.Set.t Val.tag = Val.create "free"
 
 let extract_val (type a) (type b) (tag : a Val.tag) (tag' : b Val.tag) (v : b) : a =
 match Val.eq tag tag' with
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index 33b1010213..cf1d7e81a1 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -83,3 +83,7 @@ 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
 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]. *)
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index f458f6e81f..c15331571b 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -23,8 +23,6 @@ let () = register_handler begin function
 | _ -> raise Unhandled
 end
 
-let val_exn = Tac2dyn.Val.create "ltac2:exn"
-
 type environment = valexpr Id.Map.t
 
 let empty_environment = Id.Map.empty
diff --git a/src/tac2interp.mli b/src/tac2interp.mli
index 18522c3c91..1ac26b48db 100644
--- a/src/tac2interp.mli
+++ b/src/tac2interp.mli
@@ -26,7 +26,3 @@ 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 Tac2dyn.Val.tag
-(** Toplevel representation of OCaml exceptions. Invariant: no [LtacError]
-    should be put into a value with tag [val_exn]. *)