14 files changed, 86 insertions, 6 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 08ce72932a..aefa09dbe6 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 7bdc604b88..cbf5788e48 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 0973d73ee0..9128d4042b 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 1d7019d09f..34c62043ef 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 f3e8e72bb7..c02fc5aafd 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 b70bfd83c1..f03bde68ec 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 7804cc6796..055fd68f6c 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 49ea9727c6..f27928662e 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 0000000000..be8579c2e5
--- /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 3a1faf1c77..ffe0186af0 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 ea1f2de539..30783bfad5 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 5822f5add5..6537d1ecf7 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 d04dcb8e3b..9904b73540 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 91726e8c6d..a6b8262f7f 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)