Removing dead code in Ltac2, and cleaning up a bit.

6 files changed, 9 insertions, 18 deletions

diff --git a/g_ltac2.ml4 b/g_ltac2.ml4
index 565be4a199..51919addf2 100644
--- a/g_ltac2.ml4
+++ b/g_ltac2.ml4
@@ -8,7 +8,6 @@
 
 open Pp
 open Util
-open Genarg
 open Names
 open Pcoq
 open Constrexpr
diff --git a/tac2core.ml b/tac2core.ml
index ad238e6b8f..13395c87b3 100644
--- a/tac2core.ml
+++ b/tac2core.ml
@@ -8,7 +8,6 @@
 
 open CSig
 open Pp
-open CErrors
 open Names
 open Genarg
 open Geninterp
@@ -20,10 +19,6 @@ open Proofview.Notations
 (** Standard values *)
 
 let coq_core n = KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n))
-let stdlib_prefix md =
-  MPfile (DirPath.make (List.map Id.of_string [md; "ltac2"; "Coq"]))
-let coq_stdlib md n =
-  KerName.make2 (stdlib_prefix md) (Label.of_id (Id.of_string n))
 
 let val_tag t = match val_tag t with
 | Val.Base t -> t
@@ -141,9 +136,6 @@ let err_notfocussed =
 let err_outofbounds =
   LtacError (coq_core "Out_of_bounds", [||])
 
-let err_notfound =
-  LtacError (coq_core "Not_found", [||])
-
 (** Helper functions *)
 
 let thaw f = interp_app f [v_unit]
@@ -158,10 +150,6 @@ let wrap f =
 let wrap_unit f =
   return () >>= fun () -> f (); return v_unit
 
-let wrap_exn f err =
-  return () >>= fun () ->
-    try return (f ()) with e when CErrors.noncritical e -> err
-
 let pf_apply f =
   Proofview.Goal.goals >>= function
   | [] ->
diff --git a/tac2core.mli b/tac2core.mli
index 27144bc6e2..fc90499ac6 100644
--- a/tac2core.mli
+++ b/tac2core.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Names
 open Tac2env
 open Tac2expr
 
@@ -18,6 +19,11 @@ val t_list : type_constant
 val c_nil : ltac_constant
 val c_cons : ltac_constant
 
+val t_int : type_constant
+val t_option : type_constant
+val t_string : type_constant
+val t_array : type_constant
+
 end
 
 (** {5 Ltac2 FFI} *)
@@ -50,4 +56,7 @@ val to_constr : valexpr -> EConstr.t
 val of_exn : Exninfo.iexn -> valexpr
 val to_exn : valexpr -> Exninfo.iexn
 
+val of_ident : Id.t -> valexpr
+val to_ident : valexpr -> Id.t
+
 end
diff --git a/tac2entries.ml b/tac2entries.ml
index fbfc687ee7..3959e705ed 100644
--- a/tac2entries.ml
+++ b/tac2entries.ml
@@ -13,7 +13,6 @@ open Names
 open Libnames
 open Libobject
 open Nametab
-open Tac2env
 open Tac2expr
 open Tac2print
 open Tac2intern
diff --git a/tac2env.ml b/tac2env.ml
index a36d022e4d..5ccdd018ee 100644
--- a/tac2env.ml
+++ b/tac2env.ml
@@ -8,7 +8,6 @@
 
 open CErrors
 open Util
-open Genarg
 open Names
 open Libnames
 open Tac2expr
diff --git a/tac2intern.ml b/tac2intern.ml
index 17d08b2285..756bbe3076 100644
--- a/tac2intern.ml
+++ b/tac2intern.ml
@@ -39,7 +39,6 @@ type 'a t
 val equal : elt -> elt -> bool
 val create : unit -> 'a t
 val fresh : 'a t -> elt
-val size : 'a t -> int
 val find : elt -> 'a t -> (elt * 'a option)
 val union : elt -> elt -> 'a t -> unit
 val set : elt -> 'a -> 'a t -> unit
@@ -69,8 +68,6 @@ type 'a t = {
   mutable uf_size : int;
 }
 
-let size p = p.uf_size
-
 let resize p =
   if Int.equal (Array.length p.uf_data) p.uf_size then begin
     let nsize = 2 * p.uf_size + 1 in