[general] Remove Econstr dependency from `intf`

To this extent we factor out the relevant bits to a new file,
ltac_pretype.

1 files changed, 0 insertions, 27 deletions

diff --git a/intf/glob_term.ml b/intf/glob_term.ml
index 757ba57868..508990a580 100644
--- a/intf/glob_term.ml
+++ b/intf/glob_term.ml
@@ -100,30 +100,3 @@ type 'a extended_glob_local_binder_r =
 and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t
 
 type extended_glob_local_binder = [ `any ] extended_glob_local_binder_g
-
-(** A globalised term together with a closure representing the value
-    of its free variables. Intended for use when these variables are taken
-    from the Ltac environment. *)
-type closure = {
-  idents:Id.t Id.Map.t;
-  typed: Pattern.constr_under_binders Id.Map.t ;
-  untyped:closed_glob_constr Id.Map.t }
-and closed_glob_constr = {
-  closure: closure;
-  term: glob_constr }
-
-(** Ltac variable maps *)
-type var_map = Pattern.constr_under_binders Id.Map.t
-type uconstr_var_map = closed_glob_constr Id.Map.t
-type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t
-
-type ltac_var_map = {
-  ltac_constrs : var_map;
-  (** Ltac variables bound to constrs *)
-  ltac_uconstrs : uconstr_var_map;
-  (** Ltac variables bound to untyped constrs *)
-  ltac_idents: Id.t Id.Map.t;
-  (** Ltac variables bound to identifiers *)
-  ltac_genargs : unbound_ltac_var_map;
-  (** Ltac variables bound to other kinds of arguments *)
-}