[general] Remove Econstr dependency from `intf`

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

10 files changed, 24 insertions, 25 deletions

diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index d9150a7bb..1f628803a 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -17,6 +17,7 @@ open Refiner
 open Evd
 open Locus
 open Context.Named.Declaration
+open Ltac_pretype
 
 module NamedDecl = Context.Named.Declaration
 
@@ -27,7 +28,7 @@ let instantiate_evar evk (ist,rawc) sigma =
   let filtered = Evd.evar_filtered_env evi in
   let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in
   let lvar = {
-    Glob_term.ltac_constrs = constrvars;
+    ltac_constrs = constrvars;
     ltac_uconstrs = Names.Id.Map.empty;
     ltac_idents = Names.Id.Map.empty;
     ltac_genargs = ist.Geninterp.lfun;
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 9e3a54cc8..a79a92a66 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -10,7 +10,6 @@ open Util
 open Names
 open Term
 open EConstr
-open Pattern
 open Misctypes
 open Genarg
 open Stdarg
@@ -24,7 +23,7 @@ let (wit_constr_context : (Empty.t, Empty.t, EConstr.constr) Genarg.genarg_type)
   wit
 
 (* includes idents known to be bound and references *)
-let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) =
+let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) Genarg.genarg_type) =
   let wit = Genarg.create_arg "constr_under_binders" in
   let () = register_val0 wit None in
   wit
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 1a67f6f88..d7b253a68 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -10,7 +10,6 @@ open Util
 open Names
 open EConstr
 open Misctypes
-open Pattern
 open Genarg
 open Geninterp
 
@@ -37,8 +36,8 @@ sig
 
   val of_constr : constr -> t
   val to_constr : t -> constr option
-  val of_uconstr : Glob_term.closed_glob_constr -> t
-  val to_uconstr : t -> Glob_term.closed_glob_constr option
+  val of_uconstr : Ltac_pretype.closed_glob_constr -> t
+  val to_uconstr : t -> Ltac_pretype.closed_glob_constr option
   val of_int : int -> t
   val to_int : t -> int option
   val to_list : t -> t list option
@@ -63,9 +62,9 @@ val coerce_to_hint_base : Value.t -> string
 
 val coerce_to_int : Value.t -> int
 
-val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders
+val coerce_to_constr : Environ.env -> Value.t -> Ltac_pretype.constr_under_binders
 
-val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.closed_glob_constr
+val coerce_to_uconstr : Environ.env -> Value.t -> Ltac_pretype.closed_glob_constr
 
 val coerce_to_closed_constr : Environ.env -> Value.t -> constr
 
@@ -93,4 +92,4 @@ val coerce_to_int_or_var_list : Value.t -> int or_var list
 
 val wit_constr_context : (Empty.t, Empty.t, EConstr.constr) genarg_type
 
-val wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) genarg_type
+val wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) genarg_type
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 2c36faeff..163973688 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -386,7 +386,7 @@ type ltac_call_kind =
   | LtacNameCall of ltac_constant
   | LtacAtomCall of glob_atomic_tactic_expr
   | LtacVarCall of Id.t * glob_tactic_expr
-  | LtacConstrInterp of Glob_term.glob_constr * Glob_term.ltac_var_map
+  | LtacConstrInterp of Glob_term.glob_constr * Ltac_pretype.ltac_var_map
 
 type ltac_trace = ltac_call_kind Loc.located list
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 20f117ff4..66f124d2d 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -38,6 +38,7 @@ open Tacintern
 open Taccoerce
 open Proofview.Notations
 open Context.Named.Declaration
+open Ltac_pretype
 
 let ltac_trace_info = Tactic_debug.ltac_trace_info
 
@@ -551,7 +552,6 @@ let interp_fresh_id ist env sigma l =
 
 (* Extract the uconstr list from lfun *)
 let extract_ltac_constr_context ist env sigma =
-  let open Glob_term in
   let add_uconstr id v map =
     try Id.Map.add id (coerce_to_uconstr env v) map
     with CannotCoerceTo _ -> map
@@ -602,10 +602,10 @@ let interp_gen kind ist pattern_mode flags env sigma c =
   let { closure = constrvars ; term } =
     interp_glob_closure ist env sigma ~kind:kind_for_intern ~pattern_mode c in
   let vars = {
-    Glob_term.ltac_constrs = constrvars.typed;
-    Glob_term.ltac_uconstrs = constrvars.untyped;
-    Glob_term.ltac_idents = constrvars.idents;
-    Glob_term.ltac_genargs = ist.lfun;
+    ltac_constrs = constrvars.typed;
+    ltac_uconstrs = constrvars.untyped;
+    ltac_idents = constrvars.idents;
+    ltac_genargs = ist.lfun;
   } in
   (* Jason Gross: To avoid unnecessary modifications to tacinterp, as
       suggested by Arnaud Spiwack, we run push_trace immediately.  We do
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index d0a0a81d4..5f2723a1e 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -44,7 +44,7 @@ val f_avoid_ids : Id.Set.t TacStore.field
 val f_debug : debug_info TacStore.field
 
 val extract_ltac_constr_values : interp_sign -> Environ.env ->
-  Pattern.constr_under_binders Id.Map.t
+  Ltac_pretype.constr_under_binders Id.Map.t
 (** Given an interpretation signature, extract all values which are coercible to
     a [constr]. *)
 
@@ -57,7 +57,7 @@ val get_debug : unit -> debug_info
 val type_uconstr :
   ?flags:Pretyping.inference_flags ->
   ?expected_type:Pretyping.typing_constraint ->
-  Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open
+  Geninterp.interp_sign -> Ltac_pretype.closed_glob_constr -> constr Tactypes.delayed_open
 
 (** Adds an interpretation function for extra generic arguments *)
 
@@ -79,10 +79,10 @@ val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map ->
 
 val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map ->
   ?kind:Pretyping.typing_constraint -> ?pattern_mode:bool -> glob_constr_and_expr ->
-  Glob_term.closed_glob_constr
+  Ltac_pretype.closed_glob_constr
 
 val interp_uconstr : interp_sign -> Environ.env -> Evd.evar_map ->
-  glob_constr_and_expr -> Glob_term.closed_glob_constr
+  glob_constr_and_expr -> Ltac_pretype.closed_glob_constr
 
 val interp_constr_gen : Pretyping.typing_constraint -> interp_sign ->
   Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Evd.evar_map * constr
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 5394b1e11..a669692fc 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -363,7 +363,7 @@ let explain_ltac_call_trace last trace loc =
   | Tacexpr.LtacAtomCall te ->
       quote (Pptactic.pr_glob_tactic (Global.env())
               (Tacexpr.TacAtom (Loc.tag te)))
-  | Tacexpr.LtacConstrInterp (c, { Glob_term.ltac_constrs = vars }) ->
+  | Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) ->
       quote (Printer.pr_glob_constr_env (Global.env()) c) ++
         (if not (Id.Map.is_empty vars) then
           strbrk " (with " ++
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index 63b8cc482..31afab046 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -22,7 +22,7 @@ module NamedDecl = Context.Named.Declaration
     those of {!Matching.matching_result}), and a {!Term.constr}
     substitution mapping corresponding to matched hypotheses. *)
 type 'a t = {
-  subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ;
+  subst : Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map ;
   context : EConstr.constr Id.Map.t;
   terms : EConstr.constr Id.Map.t;
   lhs : 'a;
@@ -36,8 +36,8 @@ type 'a t = {
 (** Some of the functions of {!Matching} return the substitution with a
     [patvar_map] instead of an [extended_patvar_map]. [adjust] coerces
     substitution of the former type to the latter. *)
-let adjust : Constr_matching.bound_ident_map * Pattern.patvar_map ->
-             Constr_matching.bound_ident_map * Pattern.extended_patvar_map =
+let adjust : Constr_matching.bound_ident_map * Ltac_pretype.patvar_map ->
+             Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map =
   fun (l, lc) -> (l, Id.Map.map (fun c -> [], c) lc)
 
 
diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli
index 01334d36c..955f8105f 100644
--- a/plugins/ltac/tactic_matching.mli
+++ b/plugins/ltac/tactic_matching.mli
@@ -18,7 +18,7 @@
     those of {!Matching.matching_result}), and a {!Term.constr}
     substitution mapping corresponding to matched hypotheses. *)
 type 'a t = {
-  subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ;
+  subst : Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map ;
   context : EConstr.constr Names.Id.Map.t;
   terms : EConstr.constr Names.Id.Map.t;
   lhs : 'a;
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index d37c676e3..1f2d02093 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -227,7 +227,7 @@ let isAppInd gl c =
 let interp_refine ist gl rc =
   let constrvars = Tacinterp.extract_ltac_constr_values ist (pf_env gl) in
   let vars = { Glob_ops.empty_lvar with
-    Glob_term.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun
+    Ltac_pretype.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun
   } in
   let kind = Pretyping.OfType (pf_concl gl) in
   let flags = {