[general] Remove Econstr dependency from `intf`

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

37 files changed, 209 insertions, 152 deletions

diff --git a/API/API.ml b/API/API.ml
index bf99d0feb..6e61063e4 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -131,6 +131,7 @@ module Geninterp = Geninterp
 (******************************************************************************)
 (* Pretyping                                                                  *)
 (******************************************************************************)
+module Ltac_pretype = Ltac_pretype
 module Locusops = Locusops
 module Pretype_errors = Pretype_errors
 module Reductionops = Reductionops
diff --git a/API/API.mli b/API/API.mli
index a41009fa2..35fc35ea3 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2757,13 +2757,6 @@ sig
     | PFix of Term.fixpoint
     | PCoFix of Term.cofixpoint
 
-  type constr_under_binders = Names.Id.t list * EConstr.constr
-
-  (** Types of substitutions with or w/o bound variables *)
-
-  type patvar_map = EConstr.constr Names.Id.Map.t
-  type extended_patvar_map = constr_under_binders Names.Id.Map.t
-
 end
 
 module Namegen :
@@ -3185,34 +3178,6 @@ sig
    type any_glob_constr =
    | AnyGlobConstr : 'r glob_constr_g -> any_glob_constr
 
-   (** 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 : Names.Id.t Names.Id.Map.t;
-     typed  : Pattern.constr_under_binders Names.Id.Map.t ;
-     untyped: closed_glob_constr Names.Id.Map.t }
-   and closed_glob_constr = {
-     closure: closure;
-     term: glob_constr }
-
-   (** Ltac variable maps *)
-   type var_map = Pattern.constr_under_binders Names.Id.Map.t
-   type uconstr_var_map = closed_glob_constr Names.Id.Map.t
-   type unbound_ltac_var_map = Geninterp.Val.t Names.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: Names.Id.t Names.Id.Map.t;
-     (** Ltac variables bound to identifiers *)
-     ltac_genargs : unbound_ltac_var_map;
-     (** Ltac variables bound to other kinds of arguments *)
-   }
-
 end
 
 module Notation_term :
@@ -3276,6 +3241,79 @@ end
 (* Modules from pretyping/                                              *)
 (************************************************************************)
 
+module Ltac_pretype :
+sig
+open Names
+open Glob_term
+
+(** {5 Maps of pattern variables} *)
+
+(** Type [constr_under_binders] is for representing the term resulting
+    of a matching. Matching can return terms defined in a some context
+    of named binders; in the context, variable names are ordered by
+    (<) and referred to by index in the term Thanks to the canonical
+    ordering, a matching problem like
+
+    [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]]
+
+    will be accepted. Thanks to the reference by index, a matching
+    problem like
+
+    [match ... with [(fun x => ?p)] => [forall x => p]]
+
+    will work even if [x] is also the name of an existing goal
+    variable.
+
+    Note: we do not keep types in the signature. Besides simplicity,
+    the main reason is that it would force to close the signature over
+    binders that occur only in the types of effective binders but not
+    in the term itself (e.g. for a term [f x] with [f:A -> True] and
+    [x:A]).
+
+    On the opposite side, by not keeping the types, we loose
+    opportunity to propagate type informations which otherwise would
+    not be inferable, as e.g. when matching [forall x, x = 0] with
+    pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in
+    expression [forall x, h = x] where nothing tells how the type of x
+    could be inferred. We also loose the ability of typing ltac
+    variables before calling the right-hand-side of ltac matching clauses. *)
+
+type constr_under_binders = Id.t list * EConstr.constr
+
+(** Types of substitutions with or w/o bound variables *)
+
+type patvar_map = EConstr.constr Id.Map.t
+type extended_patvar_map = constr_under_binders Id.Map.t
+
+(** 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: 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 = 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 *)
+}
+
+end
+
 module Locusops :
 sig
   val clause_with_generic_occurrences : 'a Locus.clause_expr -> bool
@@ -3513,7 +3551,7 @@ sig
   val map_glob_constr :
     (Glob_term.glob_constr -> Glob_term.glob_constr) -> Glob_term.glob_constr -> Glob_term.glob_constr
 
-  val empty_lvar : Glob_term.ltac_var_map
+  val empty_lvar : Ltac_pretype.ltac_var_map
 
 end
 
@@ -3529,7 +3567,7 @@ sig
   val subst_pattern : Mod_subst.substitution -> Pattern.constr_pattern -> Pattern.constr_pattern
   val pattern_of_constr : Environ.env -> Evd.evar_map -> Constr.t -> Pattern.constr_pattern
   val instantiate_pattern : Environ.env ->
-    Evd.evar_map -> Pattern.extended_patvar_map ->
+    Evd.evar_map -> Ltac_pretype.extended_patvar_map ->
     Pattern.constr_pattern -> Pattern.constr_pattern
 end
 
@@ -3542,16 +3580,16 @@ sig
   val is_matching : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> bool
   val extended_matches :
     Environ.env -> Evd.evar_map -> binding_bound_vars * Pattern.constr_pattern ->
-    EConstr.constr -> bound_ident_map * Pattern.extended_patvar_map
+    EConstr.constr -> bound_ident_map * Ltac_pretype.extended_patvar_map
   exception PatternMatchingFailure
   type matching_result =
-    { m_sub : bound_ident_map * Pattern.patvar_map;
+    { m_sub : bound_ident_map * Ltac_pretype.patvar_map;
       m_ctx : EConstr.constr }
   val match_subterm_gen : Environ.env -> Evd.evar_map ->
                           bool ->
                           binding_bound_vars * Pattern.constr_pattern -> EConstr.constr ->
                           matching_result IStream.t
-  val matches : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> Pattern.patvar_map
+  val matches : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> Ltac_pretype.patvar_map
 end
 
 module Tacred :
@@ -4082,7 +4120,7 @@ sig
     }
 
   val understand_ltac : inference_flags ->
-                        Environ.env -> Evd.evar_map -> Glob_term.ltac_var_map ->
+                        Environ.env -> Evd.evar_map -> Ltac_pretype.ltac_var_map ->
                         typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.t
   val understand_tcc : ?flags:inference_flags -> Environ.env -> Evd.evar_map ->
                        ?expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr
@@ -4091,11 +4129,11 @@ sig
   val check_evars : Environ.env -> Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit
   val register_constr_interp0 :
     ('r, 'g, 't) Genarg.genarg_type ->
-    (Glob_term.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit
+    (Ltac_pretype.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit
   val all_and_fail_flags : inference_flags
   val ise_pretype_gen :
     inference_flags -> Environ.env -> Evd.evar_map ->
-    Glob_term.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr
+    Ltac_pretype.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr
 end
 
 module Unification :
@@ -4203,7 +4241,7 @@ sig
   val wit_int_or_var : (int Misctypes.or_var, int Misctypes.or_var, int) Genarg.genarg_type
   val wit_ref : (Libnames.reference, Globnames.global_reference Loc.located Misctypes.or_var, Globnames.global_reference) Genarg.genarg_type
   val wit_clause_dft_concl :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) Genarg.genarg_type
-  val wit_uconstr : (Constrexpr.constr_expr , Tactypes.glob_constr_and_expr, Glob_term.closed_glob_constr) Genarg.genarg_type
+  val wit_uconstr : (Constrexpr.constr_expr , Tactypes.glob_constr_and_expr, Ltac_pretype.closed_glob_constr) Genarg.genarg_type
   val wit_red_expr :
     ((Constrexpr.constr_expr,Libnames.reference Misctypes.or_by_notation,Constrexpr.constr_expr) Genredexpr.red_expr_gen,
      (Tactypes.glob_constr_and_expr,Names.evaluable_global_reference Misctypes.and_short_name Misctypes.or_var,Tactypes.glob_constr_pattern_and_expr) Genredexpr.red_expr_gen,
@@ -4456,7 +4494,7 @@ end
 
 module Evar_refiner :
 sig
-  type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr
+  type glob_constr_ltac_closure = Ltac_pretype.ltac_var_map * Glob_term.glob_constr
 
   val w_refine : Evar.t * Evd.evar_info ->
                  glob_constr_ltac_closure -> Evd.evar_map -> Evd.evar_map
@@ -4994,16 +5032,16 @@ sig
   val pr_econstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
   val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t
   val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t
-  val pr_closed_glob : Glob_term.closed_glob_constr -> Pp.t
+  val pr_closed_glob : Ltac_pretype.closed_glob_constr -> Pp.t
   val pr_lglob_constr : Glob_term.glob_constr -> Pp.t
   val pr_leconstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
   val pr_leconstr : EConstr.constr -> Pp.t
   val pr_global : Globnames.global_reference -> Pp.t
-  val pr_lconstr_under_binders : Pattern.constr_under_binders -> Pp.t
-  val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.t
+  val pr_lconstr_under_binders : Ltac_pretype.constr_under_binders -> Pp.t
+  val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t
 
-  val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.t
-  val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Glob_term.closed_glob_constr -> Pp.t
+  val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t
+  val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Ltac_pretype.closed_glob_constr -> Pp.t
   val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.t
   val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.t
   val pr_ltype : Term.types -> Pp.t
@@ -5158,7 +5196,7 @@ module Tactics :
 sig
   open Proofview
 
-  type change_arg = Pattern.patvar_map -> Evd.evar_map -> Evd.evar_map * EConstr.constr
+  type change_arg = Ltac_pretype.patvar_map -> Evd.evar_map -> Evd.evar_map * EConstr.constr
   type tactic_reduction = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
 
   type elim_scheme =
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ffa8fffdf..70f7c4283 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -108,8 +108,7 @@ let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l)
 let ppunbound_ltac_var_map l = ppidmap (fun _ arg ->
   str"<genarg:" ++ pr_argument_type(genarg_tag arg) ++ str">")
 
-open Glob_term
-
+open Ltac_pretype
 let rec pr_closure {idents=idents;typed=typed;untyped=untyped} =
   hov 1 (str"{idents=" ++ prididmap idents ++ str";" ++ spc() ++
          str"typed=" ++ prconstrunderbindersidmap typed ++ str";" ++ spc() ++
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 593580fb7..b2df449c5 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -19,6 +19,7 @@ open Constrexpr
 open Notation_term
 open Notation
 open Misctypes
+open Ltac_pretype
 
 (** Translation of pattern, cases pattern, glob_constr and term into syntax
    trees for printing *)
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index dffbd6659..ed00fe296 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -51,7 +51,7 @@ val wit_sort_family : (Sorts.family, unit, unit) genarg_type
 
 val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
 
-val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
+val wit_uconstr : (constr_expr , glob_constr_and_expr, Ltac_pretype.closed_glob_constr) genarg_type
 
 val wit_open_constr :
   (constr_expr, glob_constr_and_expr, constr) genarg_type
diff --git a/intf/glob_term.ml b/intf/glob_term.ml
index 757ba5786..508990a58 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 *)
-}
diff --git a/intf/pattern.ml b/intf/pattern.ml
index 2ab526984..16c480735 100644
--- a/intf/pattern.ml
+++ b/intf/pattern.ml
@@ -11,45 +11,6 @@ open Globnames
 open Term
 open Misctypes
 
-(** {5 Maps of pattern variables} *)
-
-(** Type [constr_under_binders] is for representing the term resulting
-    of a matching. Matching can return terms defined in a some context
-    of named binders; in the context, variable names are ordered by
-    (<) and referred to by index in the term Thanks to the canonical
-    ordering, a matching problem like
-
-    [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]]
-
-    will be accepted. Thanks to the reference by index, a matching
-    problem like
-
-    [match ... with [(fun x => ?p)] => [forall x => p]]
-
-    will work even if [x] is also the name of an existing goal
-    variable.
-
-    Note: we do not keep types in the signature. Besides simplicity,
-    the main reason is that it would force to close the signature over
-    binders that occur only in the types of effective binders but not
-    in the term itself (e.g. for a term [f x] with [f:A -> True] and
-    [x:A]).
-
-    On the opposite side, by not keeping the types, we loose
-    opportunity to propagate type informations which otherwise would
-    not be inferable, as e.g. when matching [forall x, x = 0] with
-    pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in
-    expression [forall x, h = x] where nothing tells how the type of x
-    could be inferred. We also loose the ability of typing ltac
-    variables before calling the right-hand-side of ltac matching clauses. *)
-
-type constr_under_binders = Id.t list * EConstr.constr
-
-(** Types of substitutions with or w/o bound variables *)
-
-type patvar_map = EConstr.constr Id.Map.t
-type extended_patvar_map = constr_under_binders Id.Map.t
-
 (** {5 Patterns} *)
 
 type case_info_pattern =
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 = {
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 08ce72932..aefa09dbe 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -33,6 +33,7 @@ open Evarsolve
 open Evarconv
 open Evd
 open Context.Rel.Declaration
+open Ltac_pretype
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
@@ -245,7 +246,7 @@ let push_history_pattern n pci cont =
 
 type 'a pattern_matching_problem =
     { env       : env;
-      lvar      : Glob_term.ltac_var_map;
+      lvar      : Ltac_pretype.ltac_var_map;
       evdref    : evar_map ref;
       pred      : constr;
       tomatch   : tomatch_stack;
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 7bdc604b8..cbf5788e4 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -14,6 +14,7 @@ open EConstr
 open Inductiveops
 open Glob_term
 open Evarutil
+open Ltac_pretype
 
 (** {5 Compilation of pattern-matching } *)
 
@@ -101,7 +102,7 @@ and pattern_continuation =
 
 type 'a pattern_matching_problem =
     { env       : env;
-      lvar      : Glob_term.ltac_var_map;
+      lvar      : Ltac_pretype.ltac_var_map;
       evdref    : evar_map ref;
       pred      : constr;
       tomatch   : tomatch_stack;
@@ -119,11 +120,11 @@ val prepare_predicate : ?loc:Loc.t ->
             Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) ->
            Environ.env ->
            Evd.evar_map ->
-           Glob_term.ltac_var_map ->
+           Ltac_pretype.ltac_var_map ->
            (types * tomatch_type) list ->
            (rel_context * rel_context) list ->
            constr option ->
            glob_constr option -> (Evd.evar_map * Names.name list * constr) list
 
 val make_return_predicate_ltac_lvar : Evd.evar_map -> Names.name ->
-  Glob_term.glob_constr -> constr -> Glob_term.ltac_var_map -> Glob_term.ltac_var_map
+  Glob_term.glob_constr -> constr -> Ltac_pretype.ltac_var_map -> ltac_var_map
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 0973d73ee..9128d4042 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -22,6 +22,7 @@ open Pattern
 open Patternops
 open Misctypes
 open Context.Rel.Declaration
+open Ltac_pretype
 (*i*)
 
 (* Given a term with second-order variables in it,
diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli
index 1d7019d09..34c62043e 100644
--- a/pretyping/constr_matching.mli
+++ b/pretyping/constr_matching.mli
@@ -13,6 +13,7 @@ open Term
 open EConstr
 open Environ
 open Pattern
+open Ltac_pretype
 
 type binding_bound_vars = Id.Set.t
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f3e8e72bb..c02fc5aaf 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -27,6 +27,7 @@ open Mod_subst
 open Misctypes
 open Decl_kinds
 open Context.Named.Declaration
+open Ltac_pretype
 
 type _ delay =
 | Now : 'a delay
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index b70bfd83c..f03bde68e 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -15,6 +15,7 @@ open Termops
 open Mod_subst
 open Misctypes
 open Evd
+open Ltac_pretype
 
 type _ delay =
 | Now : 'a delay
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 7804cc679..055fd68f6 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -13,6 +13,7 @@ open Globnames
 open Misctypes
 open Glob_term
 open Evar_kinds
+open Ltac_pretype
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
 
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 49ea9727c..f27928662 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -84,5 +84,5 @@ val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob
 
 val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list
 
-val ltac_interp_name : Glob_term.ltac_var_map -> Names.name -> Names.name
-val empty_lvar : Glob_term.ltac_var_map
+val ltac_interp_name : Ltac_pretype.ltac_var_map -> Names.name -> Names.name
+val empty_lvar : Ltac_pretype.ltac_var_map
diff --git a/pretyping/ltac_pretype.ml b/pretyping/ltac_pretype.ml
new file mode 100644
index 000000000..be8579c2e
--- /dev/null
+++ b/pretyping/ltac_pretype.ml
@@ -0,0 +1,68 @@
+open Names
+open Glob_term
+
+(** {5 Maps of pattern variables} *)
+
+(** Type [constr_under_binders] is for representing the term resulting
+    of a matching. Matching can return terms defined in a some context
+    of named binders; in the context, variable names are ordered by
+    (<) and referred to by index in the term Thanks to the canonical
+    ordering, a matching problem like
+
+    [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]]
+
+    will be accepted. Thanks to the reference by index, a matching
+    problem like
+
+    [match ... with [(fun x => ?p)] => [forall x => p]]
+
+    will work even if [x] is also the name of an existing goal
+    variable.
+
+    Note: we do not keep types in the signature. Besides simplicity,
+    the main reason is that it would force to close the signature over
+    binders that occur only in the types of effective binders but not
+    in the term itself (e.g. for a term [f x] with [f:A -> True] and
+    [x:A]).
+
+    On the opposite side, by not keeping the types, we loose
+    opportunity to propagate type informations which otherwise would
+    not be inferable, as e.g. when matching [forall x, x = 0] with
+    pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in
+    expression [forall x, h = x] where nothing tells how the type of x
+    could be inferred. We also loose the ability of typing ltac
+    variables before calling the right-hand-side of ltac matching clauses. *)
+
+type constr_under_binders = Id.t list * EConstr.constr
+
+(** Types of substitutions with or w/o bound variables *)
+
+type patvar_map = EConstr.constr Id.Map.t
+type extended_patvar_map = constr_under_binders Id.Map.t
+
+(** 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: 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 = 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 *)
+}
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 3a1faf1c7..ffe0186af 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -12,6 +12,7 @@ open Glob_term
 open Mod_subst
 open Misctypes
 open Pattern
+open Ltac_pretype
 
 (** {5 Functions on patterns} *)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ea1f2de53..30783bfad 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -43,6 +43,7 @@ open Glob_term
 open Glob_ops
 open Evarconv
 open Misctypes
+open Ltac_pretype
 
 module NamedDecl = Context.Named.Declaration
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 5822f5add..6537d1ecf 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -18,6 +18,7 @@ open Evd
 open EConstr
 open Glob_term
 open Evarutil
+open Ltac_pretype
 
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index d04dcb8e3..9904b7354 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -1,3 +1,4 @@
+Ltac_pretype
 Locusops
 Pretype_errors
 Reductionops
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 91726e8c6..a6b8262f7 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -15,6 +15,7 @@ open Pattern
 open Globnames
 open Locus
 open Univ
+open Ltac_pretype
 
 type reduction_tactic_error =
     InvalidAbstraction of env * evar_map * constr * (env * Type_errors.type_error)
diff --git a/printing/printer.mli b/printing/printer.mli
index 2c9a4d70e..ba849bee6 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -14,6 +14,7 @@ open Pattern
 open Evd
 open Proof_type
 open Glob_term
+open Ltac_pretype
 
 (** These are the entry points for printing terms, context, tac, ... *)
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 48fa2202e..d38ff7512 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -14,6 +14,7 @@ open Evarutil
 open Evarsolve
 open Pp
 open Glob_term
+open Ltac_pretype
 
 (******************************************)
 (* Instantiation of existential variables *)
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 5d6971596..a0e3b718a 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -8,6 +8,7 @@
 
 open Evd
 open Glob_term
+open Ltac_pretype
 
 (** Refinement of existential variables. *)
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 7e6d83b10..d4e9555f3 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -15,6 +15,7 @@ open Proof_type
 open Redexpr
 open Pattern
 open Locus
+open Ltac_pretype
 
 (** Operations for handling terms under a local typing context. *)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e8a78d72d..6ab643239 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -839,7 +839,7 @@ let e_change_in_hyp redfun (id,where) =
     (convert_hyp c)
   end
 
-type change_arg = Pattern.patvar_map -> evar_map -> evar_map * EConstr.constr
+type change_arg = Ltac_pretype.patvar_map -> evar_map -> evar_map * EConstr.constr
 
 let make_change_arg c pats sigma = (sigma, replace_vars (Id.Map.bindings pats) c)
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index e07d514cd..32923ea81 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -21,6 +21,7 @@ open Unification
 open Misctypes
 open Tactypes
 open Locus
+open Ltac_pretype
 
 (** Main tactics defined in ML. This file is huge and should probably be split
     in more reasonable units at some point. Because of its size and age, the