Added support for Ltac-matching terms with variables bound in the pattern

- Instances found by matching.ml now collect the set of bound
  variables they possibly depend on in the pattern (see type
  Pattern.extended_patvar_map); the variables names are canonically
  ordered so that non-linear matching takes actual names into account.
- Removed typing of matching constr instances in advance (in
  tacinterp.ml) and did it only at use time (in pretyping.ml). Drawback
  is that we may have to re-type several times the same term but it is
  necessary for considering terms with locally bound variables of which
  we do not keep the type (and if even we had kept the type, we would have
  to adjust the indices to the actual context the term occurs).
- A bit of documentation of pattern.mli, matching.mli and pretyping.mli.
- Incidentally add env while printing idtac messages. It seems more correct
  and I hope I did not break some intended existing behavior.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13080 85f007b7-540e-0410-9357-904b9bb8a0f7

23 files changed, 339 insertions, 168 deletions

diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 597505686..cf5a58eea 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -122,6 +122,7 @@ let pr_rawsort = function
 let pr_id = pr_id
 let pr_name = pr_name
 let pr_qualid = pr_qualid
+let pr_patvar = pr_id
 
 let pr_expl_args pr (a,expl) =
   match expl with
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 2becdbcfd..afa744a50 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -46,6 +46,7 @@ val pr_sep_com :
 val pr_id : identifier -> std_ppcmds
 val pr_name : name -> std_ppcmds
 val pr_qualid : qualid -> std_ppcmds
+val pr_patvar : patvar -> std_ppcmds
 
 val pr_with_occurrences :
   ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds
diff --git a/parsing/printer.ml b/parsing/printer.ml
index d3c4ae63d..61f7e377a 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -57,6 +57,19 @@ let pr_constr t = pr_constr_env (Global.env()) t
 let pr_open_lconstr (_,c) = pr_lconstr c
 let pr_open_constr (_,c) = pr_constr c
 
+let pr_constr_under_binders_env_gen pr env (ids,c) =
+  (* Warning: clashes can occur with variables of same name in env but *)
+  (* we also need to preserve the actual names of the patterns *)
+  (* So what to do? *)
+  let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in
+  pr (push_rels_assum assums env) c
+
+let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env
+let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env
+
+let pr_constr_under_binders c = pr_constr_under_binders_env (Global.env()) c
+let pr_lconstr_under_binders c = pr_lconstr_under_binders_env (Global.env()) c
+
 let pr_type_core at_top env t =
   pr_constr_expr (extern_type at_top env t)
 let pr_ltype_core at_top env t =
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 52a090075..241650b7d 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -38,6 +38,12 @@ val pr_open_constr         : open_constr -> std_ppcmds
 val pr_open_lconstr_env    : env -> open_constr -> std_ppcmds
 val pr_open_lconstr        : open_constr -> std_ppcmds
 
+val pr_constr_under_binders_env  : env -> constr_under_binders -> std_ppcmds
+val pr_constr_under_binders      : constr_under_binders -> std_ppcmds
+
+val pr_lconstr_under_binders_env : env -> constr_under_binders -> std_ppcmds
+val pr_lconstr_under_binders     : constr_under_binders -> std_ppcmds
+
 val pr_ltype_env_at_top    : env -> types -> std_ppcmds
 val pr_ltype_env           : env -> types -> std_ppcmds
 val pr_ltype               : types -> std_ppcmds
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index f08ed7db6..4ea9c99b7 100644
--- a/plugins/field/field.ml4
+++ b/plugins/field/field.ml4
@@ -154,7 +154,7 @@ let field g =
       | _ -> raise Exit
     with Hipattern.NoEquationFound | Exit ->
       error "The statement is not built from Leibniz' equality" in
-  let th = VConstr (lookup (pf_env g) typ) in
+  let th = VConstr ([],lookup (pf_env g) typ) in
   (interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ())
     <:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g
 
@@ -174,8 +174,8 @@ let field_term l g =
   Coqlib.check_required_library ["Coq";"field";"LegacyField"];
   let env = (pf_env g)
   and evc = (project g) in
-  let th = valueIn (VConstr (guess_theory env evc l))
-  and nl = List.map (fun x -> valueIn (VConstr x)) (Quote.sort_subterm g l) in
+  let th = valueIn (VConstr ([],guess_theory env evc l))
+  and nl = List.map (fun x -> valueIn (VConstr ([],x))) (Quote.sort_subterm g l) in
   (List.fold_right
     (fun c a ->
      let tac = (Tacinterp.interp <:tactic<(Field_Term $th $c)>>) in
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 0f8c2f010..4782e001a 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -206,7 +206,7 @@ let exec_tactic env n f args =
   !res
 
 let constr_of = function
-  | VConstr c -> c
+  | VConstr ([],c) -> c
   | _ -> failwith "Ring.exec_tactic: anomaly"
 
 let stdlib_modules =
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 87c67cc14..80527f01d 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -105,14 +105,24 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
       if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
       else id
 
-  let pretype_id loc env (lvar,unbndltacvars) id =
+  let invert_ltac_bound_name env id0 id =
+    try mkRel (pi1 (lookup_rel_id id (rel_context env)))
+    with Not_found ->
+      errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
+	str " depends on pattern variable name " ++ pr_id id ++
+	str " which is not bound in current context")
+
+  let pretype_id loc env sigma (lvar,unbndltacvars) id =
     let id = strip_meta id in (* May happen in tactics defined by Grammar *)
       try
 	let (n,_,typ) = lookup_rel_id id (rel_context env) in
 	  { uj_val  = mkRel n; uj_type = lift n typ }
       with Not_found ->
 	try
-	  List.assoc id lvar
+	  let (ids,c) = List.assoc id lvar in
+	  let subst = List.map (invert_ltac_bound_name env id) ids in
+	  let c = substl subst c in
+	  { uj_val = c; uj_type = Retyping.get_type_of env sigma c }
 	with Not_found ->
 	  try
 	    let (_,_,typ) = lookup_named id env in
@@ -170,7 +180,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 
     | RVar (loc, id) ->
 	inh_conv_coerce_to_tycon loc env evdref
-	  (pretype_id loc env lvar id)
+	  (pretype_id loc env !evdref lvar id)
 	  tycon
 
     | REvar (loc, ev, instopt) ->
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 2c0285ed2..ddfe5dd07 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -46,9 +46,10 @@ type bound_ident_map = (identifier * identifier) list
 
 exception PatternMatchingFailure
 
-let constrain (n,m) (names,terms as subst) =
+let constrain (n,(ids,m as x)) (names,terms as subst) =
   try
-    if eq_constr m (List.assoc n terms) then subst
+    let (ids',m') = List.assoc n terms in
+    if ids = ids' && eq_constr m m' then subst
     else raise PatternMatchingFailure
   with
       Not_found ->
@@ -56,7 +57,7 @@ let constrain (n,m) (names,terms as subst) =
           Flags.if_verbose Pp.warning
               ("Collision between bound variable "^string_of_id n^
                  " and a metavariable of same name.");
-        (names,(n,m)::terms)
+        (names,(n,x)::terms)
 
 let add_binders na1 na2 (names,terms as subst) =
   match na1, na2 with
@@ -76,7 +77,7 @@ let add_binders na1 na2 (names,terms as subst) =
 let build_lambda toabstract stk (m : constr) =
   let rec buildrec m p_0 p_1 = match p_0,p_1 with
     | (_, []) -> m
-    | (n, (na,t)::tl) ->
+    | (n, (_,na,t)::tl) ->
 	if List.mem n toabstract then
           buildrec (mkLambda (na,t,m)) (n+1) tl
         else
@@ -96,7 +97,58 @@ let same_case_structure (_,cs1,ind,_) ci2 br1 br2 =
   | Some ind -> ind = ci2.ci_ind
   | None -> cs1 = ci2.ci_cstr_ndecls
 
-let matches_core convert allow_partial_app pat c =
+let rec list_insert f a = function
+  | [] -> [a]
+  | b::l when f a b -> a::b::l
+  | b::l when a = b -> raise PatternMatchingFailure
+  | b::l -> b :: list_insert f a l
+
+let extract_bound_vars =
+  let rec aux k = function
+  | ([],_) -> []
+  | (n::l,(na1,na2,_)::stk) when k = n ->
+      begin match na1,na2 with
+      | Name id1,Name _ -> list_insert (<) id1 (aux (k+1) (l,stk))
+      | Name _,Anonymous -> anomaly "Unnamed bound variable"
+      | Anonymous,_ -> raise PatternMatchingFailure
+      end
+  | (l,_::stk) -> aux (k+1) (l,stk)
+  | (_,[]) -> assert false
+  in aux 1
+
+let dummy_constr = mkProp
+
+let rec make_renaming ids = function
+  | (Name id,Name _,_)::stk ->
+      let renaming = make_renaming ids stk in
+      (try mkRel (list_index id ids) :: renaming
+       with Not_found -> dummy_constr :: renaming)
+  | (_,_,_)::stk ->
+      dummy_constr :: make_renaming ids stk
+  | [] ->
+      []
+
+let merge_binding allow_bound_rels stk n cT subst =
+  let depth = List.length stk in
+  let c =
+    if depth = 0 then
+      (* Optimization *)
+      ([],cT)
+    else
+      let frels = Intset.elements (free_rels cT) in
+      let frels = List.filter (fun i -> i <= depth) frels in
+      if allow_bound_rels then
+	let frels = Sort.list (<) frels in
+	let canonically_ordered_vars = extract_bound_vars (frels,stk) in
+	let renaming = make_renaming canonically_ordered_vars stk in
+	(canonically_ordered_vars, substl renaming cT)
+      else if frels = [] then
+	([],lift (-depth) cT)
+      else
+	raise PatternMatchingFailure in
+  constrain (n,c) subst
+
+let matches_core convert allow_partial_app allow_bound_rels pat c =
   let conv = match convert with
     | None -> eq_constr
     | Some (env,sigma) -> is_conv env sigma in
@@ -112,21 +164,11 @@ let matches_core convert allow_partial_app pat c =
 	      args in
 	  let frels = Intset.elements (free_rels cT) in
 	  if list_subset frels relargs then
-	    constrain (n,build_lambda relargs stk cT) subst
+	    constrain (n,([],build_lambda relargs stk cT)) subst
 	  else
 	    raise PatternMatchingFailure
 
-      | PMeta (Some n), m ->
-	  let depth = List.length stk in
-          if depth = 0 then
-            (* Optimisation *)
-            constrain (n,cT) subst
-          else
-	    let frels = Intset.elements (free_rels cT) in
-            if List.for_all (fun i -> i > depth) frels then
-	      constrain (n,lift (-depth) cT) subst
-            else
-	      raise PatternMatchingFailure
+      | PMeta (Some n), m -> merge_binding allow_bound_rels stk n cT subst
 
       | PMeta None, m -> subst
 
@@ -151,14 +193,8 @@ let matches_core convert allow_partial_app pat c =
           let p = Array.length args2 - Array.length args1 in
           if p>=0 then
             let args21, args22 = array_chop p args2 in
-            let subst =
-	      let depth = List.length stk in
-              let c = mkApp(c2,args21) in
-	      let frels = Intset.elements (free_rels c) in
-              if List.for_all (fun i -> i > depth) frels then
-	        constrain (n,lift (-depth) c) subst
-              else
-	        raise PatternMatchingFailure in
+	    let c = mkApp(c2,args21) in
+            let subst = merge_binding allow_bound_rels stk n c subst in
             array_fold_left2 (sorec stk) subst args1 args22
           else raise PatternMatchingFailure
 
@@ -167,15 +203,15 @@ let matches_core convert allow_partial_app pat c =
          with Invalid_argument _ -> raise PatternMatchingFailure)
 
       | PProd (na1,c1,d1), Prod(na2,c2,d2) ->
-	  sorec ((na2,c2)::stk)
+	  sorec ((na1,na2,c2)::stk)
             (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2
 
       | PLambda (na1,c1,d1), Lambda(na2,c2,d2) ->
-	  sorec ((na2,c2)::stk)
+	  sorec ((na1,na2,c2)::stk)
             (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2
 
       | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) ->
-	  sorec ((na2,t2)::stk)
+	  sorec ((na1,na2,t2)::stk)
             (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2
 
       | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
@@ -184,8 +220,10 @@ let matches_core convert allow_partial_app pat c =
 	  let n = rel_context_length ctx in
           let n' = rel_context_length ctx' in
 	  if noccur_between 1 n b2 & noccur_between 1 n' b2' then
-	    let s = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx in
-	    let s' = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx' in
+	    let s =
+	      List.fold_left (fun l (na,_,t) -> (Anonymous,na,t)::l) stk ctx in
+	    let s' =
+	      List.fold_left (fun l (na,_,t) -> (Anonymous,na,t)::l) stk ctx' in
 	    let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
   	    sorec s' (sorec s (sorec stk subst a1 a2) b1 b2) b1' b2'
           else
@@ -206,16 +244,20 @@ let matches_core convert allow_partial_app pat c =
   let names,terms = sorec [] ([],[]) pat c in
   (names,Sort.list (fun (a,_) (b,_) -> a<b) terms)
 
-let extended_matches = matches_core None true
+let matches_core_closed convert allow_partial_app pat c =
+  let names,subst = matches_core convert allow_partial_app false pat c in
+  (names, List.map (fun (a,(_,b)) -> (a,b)) subst)
+
+let extended_matches = matches_core None true true
 
-let matches c p = snd (matches_core None true c p)
+let matches c p = snd (matches_core_closed None true c p)
 
 let special_meta = (-1)
 
 (* Tells if it is an authorized occurrence and if the instance is closed *)
 let authorized_occ partial_app closed pat c mk_ctx next =
   try
-    let sigma = matches_core None partial_app pat c in
+    let sigma = matches_core_closed None partial_app pat c in
     if closed && not (List.for_all (fun (_,c) -> closed0 c) (snd sigma))
     then next ()
     else sigma, mk_ctx (mkMeta special_meta), next
@@ -308,7 +350,7 @@ let is_matching_appsubterm ?(closed=true) pat c =
   with PatternMatchingFailure -> false
 
 let matches_conv env sigma c p =
-  snd (matches_core (Some (env,sigma)) false c p)
+  snd (matches_core_closed (Some (env,sigma)) false c p)
 
 let is_matching_conv env sigma pat n =
   try let _ = matches_conv env sigma pat n in true
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 95314054e..eb9c8fc8c 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -6,18 +6,25 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
+(** This module implements pattern-matching on terms *)
+
 open Names
 open Term
 open Environ
 open Pattern
 open Termops
 
-(** {6 This modules implements pattern-matching on terms } *)
-
+(** [PatternMatchingFailure] is the exception raised when pattern
+  matching fails *)
 exception PatternMatchingFailure
 
+(** [special_meta] is the default name of the meta holding the
+   surrounding context in subterm matching *)
 val special_meta : metavariable
 
+(** [bound_ident_map] represents the result of matching binding
+   identifiers of the pattern with the binding identifiers of the term
+   matched *)
 type bound_ident_map = (identifier * identifier) list
 
 (** [matches pat c] matches [c] against [pat] and returns the resulting
@@ -31,7 +38,7 @@ val matches : constr_pattern -> constr -> patvar_map
    variables or metavariables have the same name, the metavariable,
    or else the rightmost bound variable, takes precedence *)
 val extended_matches :
-  constr_pattern -> constr -> bound_ident_map * patvar_map
+  constr_pattern -> constr -> bound_ident_map * extended_patvar_map
 
 (** [is_matching pat c] just tells if [c] matches against [pat] *)
 val is_matching : constr_pattern -> constr -> bool
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 48218f47f..59f3cde88 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -19,8 +19,10 @@ open Mod_subst
 
 (* Metavariables *)
 
+type constr_under_binders = identifier list * constr
+
 type patvar_map = (patvar * constr) list
-let pr_patvar = pr_id
+type extended_patvar_map = (patvar * constr_under_binders) list
 
 (* Patterns *)
 
@@ -143,9 +145,9 @@ let pattern_of_constr sigma t =
 let map_pattern_with_binders g f l = function
   | PApp (p,pl) -> PApp (f l p, Array.map (f l) pl)
   | PSoApp (n,pl) -> PSoApp (n, List.map (f l) pl)
-  | PLambda (n,a,b) -> PLambda (n,f l a,f (g l) b)
-  | PProd (n,a,b) -> PProd (n,f l a,f (g l) b)
-  | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g l) b)
+  | PLambda (n,a,b) -> PLambda (n,f l a,f (g n l) b)
+  | PProd (n,a,b) -> PProd (n,f l a,f (g n l) b)
+  | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g n l) b)
   | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2)
   | PCase (ci,po,p,pl) -> PCase (ci,f l po,f l p,Array.map (f l) pl)
   (* Non recursive *)
@@ -153,18 +155,40 @@ let map_pattern_with_binders g f l = function
   (* Bound to terms *)
   | PFix _ | PCoFix _ as x) -> x
 
-let map_pattern f = map_pattern_with_binders (fun () -> ()) (fun () -> f) ()
+let map_pattern f = map_pattern_with_binders (fun _ () -> ()) (fun () -> f) ()
+
+let error_instantiate_pattern id l =
+  let is = if List.length l = 1 then "is" else "are" in
+  errorlabstrm "" (str "Cannot substitute the term bound to " ++ pr_id id
+    ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l
+    ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")
 
-let rec instantiate_pattern lvar = function
-  | PVar id as x -> (try Lazy.force(List.assoc id lvar) with Not_found -> x)
+let instantiate_pattern lvar c =
+  let rec aux vars = function
+  | PVar id as x ->
+      (try
+	let ctx,c = List.assoc id lvar in
+	try
+	  let inst =
+	    List.map (fun id -> mkRel (list_index (Name id) vars)) ctx in
+	  let c = substl inst c in
+	  snd (pattern_of_constr Evd.empty c)
+	with Not_found (* list_index failed *) ->
+	  let vars =
+	    list_map_filter (function Name id -> Some id | _ -> None) vars in
+	  error_instantiate_pattern id (list_subtract ctx vars)
+       with Not_found (* List.assoc failed *) ->
+	 x)
   | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.")
-  | c -> map_pattern (instantiate_pattern lvar) c
+  | c ->
+      map_pattern_with_binders (fun id vars -> id::vars) aux vars c in
+  aux [] c
 
 let rec liftn_pattern k n = function
   | PRel i as x -> if i >= n then PRel (i+k) else x
   | PFix x -> PFix (destFix (liftn k n (mkFix x)))
   | PCoFix x -> PCoFix (destCoFix (liftn k n (mkCoFix x)))
-  | c -> map_pattern_with_binders succ (liftn_pattern k) n c
+  | c -> map_pattern_with_binders (fun _ -> succ) (liftn_pattern k) n c
 
 let lift_pattern k = liftn_pattern k 1
 
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index d805730e9..3b61c1e43 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -6,6 +6,9 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
+(** This module defines the type of pattern used for pattern-matching
+    terms in tatics *)
+
 open Pp
 open Names
 open Sign
@@ -16,12 +19,46 @@ open Nametab
 open Rawterm
 open Mod_subst
 
-(** Pattern variables *)
+(** {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 = identifier list * constr
+
+(** Types of substitutions with or w/o bound variables *)
 
 type patvar_map = (patvar * constr) list
-val pr_patvar : patvar -> std_ppcmds
+type extended_patvar_map = (patvar * constr_under_binders) list
 
-(** Patterns *)
+(** {5 Patterns} *)
 
 type constr_pattern =
   | PRef of global_reference
@@ -41,6 +78,8 @@ type constr_pattern =
   | PFix of fixpoint
   | PCoFix of cofixpoint
 
+(** {5 Functions on patterns} *)
+
 val occur_meta_pattern : constr_pattern -> bool
 
 val subst_pattern : substitution -> constr_pattern -> constr_pattern
@@ -72,6 +111,7 @@ val pattern_of_rawconstr : rawconstr ->
       patvar list * constr_pattern
 
 val instantiate_pattern :
-  (identifier * constr_pattern Lazy.t) list -> constr_pattern -> constr_pattern
+  (identifier * (identifier list * constr)) list ->
+  constr_pattern -> constr_pattern
 
 val lift_pattern : int -> constr_pattern -> constr_pattern
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 71a21f6c8..e63b9a234 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -45,8 +45,10 @@ open Evarconv
 open Pattern
 
 type typing_constraint = OfType of types option | IsType
-type var_map = (identifier * unsafe_judgment) list
+type var_map = (identifier * constr_under_binders) list
 type unbound_ltac_var_map = (identifier * identifier option) list
+type ltac_var_map = var_map * unbound_ltac_var_map
+type rawconstr_ltac_closure = ltac_var_map * rawconstr
 
 (************************************************************************)
 (* This concerns Cases *)
@@ -131,7 +133,7 @@ sig
   *)
 
   val understand_ltac :
-    bool -> evar_map -> env -> var_map * unbound_ltac_var_map ->
+    bool -> evar_map -> env -> ltac_var_map ->
     typing_constraint -> rawconstr -> evar_map * constr
 
   (* Standard call to get a constr from a rawconstr, resolving implicit args *)
@@ -162,18 +164,15 @@ sig
    *)
   val pretype :
     type_constraint -> env -> evar_map ref ->
-    var_map * (identifier * identifier option) list ->
-    rawconstr -> unsafe_judgment
+    ltac_var_map -> rawconstr -> unsafe_judgment
 
   val pretype_type :
     val_constraint -> env -> evar_map ref ->
-    var_map * (identifier * identifier option) list ->
-    rawconstr -> unsafe_type_judgment
+    ltac_var_map -> rawconstr -> unsafe_type_judgment
 
   val pretype_gen :
     bool -> bool -> bool -> evar_map ref -> env ->
-    var_map * (identifier * identifier option) list ->
-    typing_constraint -> rawconstr -> constr
+    ltac_var_map -> typing_constraint -> rawconstr -> constr
 
     (*i*)
 end
@@ -225,7 +224,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let check_branches_message loc env evdref c (explft,lft) =
     for i = 0 to Array.length explft - 1 do
       if not (e_cumul env evdref lft.(i) explft.(i)) then
-	let sigma =  !evdref in
+	let sigma = !evdref in
 	  error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
     done
 
@@ -243,7 +242,14 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | Anonymous -> name'
     | _ -> name
 
-  let pretype_id loc env (lvar,unbndltacvars) id =
+  let invert_ltac_bound_name env id0 id =
+    try mkRel (pi1 (lookup_rel_id id (rel_context env)))
+    with Not_found ->
+      errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
+	str " depends on pattern variable name " ++ pr_id id ++
+	str " which is not bound in current context.")
+
+  let pretype_id loc env sigma (lvar,unbndltacvars) id =
     (* Look for the binder of [id] *)
     try
       let (n,_,typ) = lookup_rel_id id (rel_context env) in
@@ -251,7 +257,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     with Not_found ->
     (* Check if [id] is an ltac variable *)
     try
-      List.assoc id lvar
+      let (ids,c) = List.assoc id lvar in
+      let subst = List.map (invert_ltac_bound_name env id) ids in
+      let c = substl subst c in
+      { uj_val = c; uj_type = Retyping.get_type_of env sigma c }
     with Not_found ->
     (* Check if [id] is a section or goal variable *)
     try
@@ -295,7 +304,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 
     | RVar (loc, id) ->
 	inh_conv_coerce_to_tycon loc env evdref
-	  (pretype_id loc env lvar id)
+	  (pretype_id loc env !evdref lvar id)
 	  tycon
 
     | REvar (loc, evk, instopt) ->
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 18a6b03a7..00eb613ab 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -6,6 +6,12 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
+(** This file implements type inference. It maps [rawconstr]
+   (i.e. untyped terms whose names are located) to [constr]. In
+   particular, it drives complex pattern-matching problems ("match")
+   into elementary ones, insertion of coercions and resolution of
+   implicit arguments. *)
+
 open Names
 open Sign
 open Term
@@ -21,8 +27,10 @@ val search_guard :
 
 type typing_constraint = OfType of types option | IsType
 
-type var_map = (identifier * unsafe_judgment) list
+type var_map = (identifier * Pattern.constr_under_binders) list
 type unbound_ltac_var_map = (identifier * identifier option) list
+type ltac_var_map = var_map * unbound_ltac_var_map
+type rawconstr_ltac_closure = ltac_var_map * rawconstr
 
 module type S =
 sig
@@ -56,7 +64,7 @@ sig
   *)
 
   val understand_ltac :
-    bool -> evar_map -> env -> var_map * unbound_ltac_var_map ->
+    bool -> evar_map -> env -> ltac_var_map ->
     typing_constraint -> rawconstr -> evar_map * constr
 
   (** Standard call to get a constr from a rawconstr, resolving implicit args *)
@@ -84,18 +92,15 @@ sig
   (** Internal of Pretyping... *)
   val pretype :
     type_constraint -> env -> evar_map ref ->
-    var_map * (identifier * identifier option) list ->
-    rawconstr -> unsafe_judgment
+    ltac_var_map -> rawconstr -> unsafe_judgment
 
   val pretype_type :
     val_constraint -> env -> evar_map ref ->
-    var_map * (identifier * identifier option) list ->
-    rawconstr -> unsafe_type_judgment
+    ltac_var_map -> rawconstr -> unsafe_type_judgment
 
   val pretype_gen :
     bool -> bool -> bool -> evar_map ref -> env ->
-    var_map * (identifier * identifier option) list ->
-    typing_constraint -> rawconstr -> constr
+    ltac_var_map -> typing_constraint -> rawconstr -> constr
 
   (**/**)
 
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index ca3bd1e80..a8debc6fd 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -17,7 +17,7 @@ open Rawterm
 (** Refinement of existential variables. *)
 
 val w_refine : evar * evar_info ->
-  (var_map * unbound_ltac_var_map) * rawconstr -> evar_map -> evar_map
+  rawconstr_ltac_closure -> evar_map -> evar_map
 
 val instantiate_pf_com :
   Evd.evar -> Topconstr.constr_expr -> Evd.evar_map -> Evd.evar_map
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 55a73c608..27b186a82 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -96,7 +96,7 @@ type ltac_call_kind =
   | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref
   | LtacVarCall of identifier * glob_tactic_expr
   | LtacConstrInterp of rawconstr *
-      ((identifier * constr) list * (identifier * identifier option) list)
+      (extended_patvar_map * (identifier * identifier option) list)
 
 type ltac_trace = (int * loc * ltac_call_kind) list
 
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index b07389cee..73be0c2b7 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -126,7 +126,7 @@ type ltac_call_kind =
   | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref
   | LtacVarCall of identifier * glob_tactic_expr
   | LtacConstrInterp of rawconstr *
-      ((identifier * constr) list * (identifier * identifier option) list)
+      (extended_patvar_map * (identifier * identifier option) list)
 
 type ltac_trace = (int * loc * ltac_call_kind) list
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 32a199e60..0448b0b22 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -543,7 +543,7 @@ let add_extern pri pat tacast local dbname =
 	(match (list_subtract tacmetas patmetas) with
 	| i::_ ->
 	    errorlabstrm "add_extern"
-	      (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound.")
+	      (str "The meta-variable ?" ++ Ppconstr.pr_patvar i ++ str" is not bound.")
 	| []  ->
 	    Lib.add_anonymous_leaf
 	      (inAutoHint(local,dbname, AddTactic [make_extern pri (Some pat) tacast])))
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index c8e6c9769..b8552a5aa 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -51,7 +51,7 @@ let instantiate n (ist,rawc) ido gl =
     if n <= 0 then error "Incorrect existential variable index.";
     let evk,_ = destEvar (List.nth evl (n-1)) in
     let evi = Evd.find sigma evk in
-    let ltac_vars = Tacinterp.extract_ltac_vars ist sigma (Evd.evar_env evi) in
+    let ltac_vars = Tacinterp.extract_ltac_constr_values ist (Evd.evar_env evi) in
     let sigma' = w_refine (evk,evi) (ltac_vars,rawc) sigma in
       tclTHEN
         (tclEVARS sigma')
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3d5f2ba1b..72064f4e5 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -81,7 +81,8 @@ type value =
   | VIntroPattern of intro_pattern_expr (* includes idents which are not *)
                         (* bound as in "Intro H" but which may be bound *)
                         (* later, as in "tac" in "Intro H; tac" *)
-  | VConstr of constr   (* includes idents known to be bound and references *)
+  | VConstr of constr_under_binders
+                        (* includes idents known to be bound and references *)
   | VConstr_context of constr
   | VList of value list
   | VRec of (identifier*value) list ref * glob_tactic_expr
@@ -125,7 +126,10 @@ let rec pr_value env = function
   | VVoid -> str "()"
   | VInteger n -> int n
   | VIntroPattern ipat -> pr_intro_pattern (dloc,ipat)
-  | VConstr c | VConstr_context c ->
+  | VConstr c ->
+      (match env with Some env ->
+	pr_lconstr_under_binders_env env c | _ -> str "a term")
+  | VConstr_context c ->
       (match env with Some env -> pr_lconstr_env env c | _ -> str "a term")
   | (VRTactic _ | VFun _ | VRec _) -> str "a tactic"
   | VList [] -> str "an empty list"
@@ -638,10 +642,10 @@ let declare_xml_printer f = print_xml_term := f
 let internalise_tacarg ch = G_xml.parse_tactic_arg ch
 
 let extern_tacarg ch env sigma = function
-  | VConstr c -> !print_xml_term ch env sigma c
+  | VConstr ([],c) -> !print_xml_term ch env sigma c
   | VRTactic _ | VFun _ | VVoid | VInteger _ | VConstr_context _
-  | VIntroPattern _  | VRec _ | VList _ ->
-      error "Only externing of terms is implemented."
+  | VIntroPattern _  | VRec _ | VList _ | VConstr _ ->
+      error "Only externing of closed terms is implemented."
 
 let extern_request ch req gl la =
   output_string ch "<REQUEST req=\""; output_string ch req;
@@ -653,7 +657,7 @@ let value_of_ident id = VIntroPattern (IntroIdentifier id)
 
 let extend_values_with_bindings (ln,lm) lfun =
   let lnames = List.map (fun (id,id') ->(id,value_of_ident id')) ln in
-  let lmatch = List.map (fun (id,c) -> (id,VConstr c)) lm in
+  let lmatch = List.map (fun (id,(ids,c)) -> (id,VConstr (ids,c))) lm in
   (* For compatibility, bound variables are visible only if no other
      binding of the same name exists *)
   lmatch@lfun@lnames
@@ -988,7 +992,7 @@ and intern_genarg ist x =
 (* Evaluation/interpretation *)
 
 let constr_to_id loc = function
-  | VConstr c when isVar c -> destVar c
+  | VConstr ([],c) when isVar c -> destVar c
   | _ -> invalid_arg_loc (loc, "Not an identifier")
 
 let constr_to_qid loc c =
@@ -1039,7 +1043,7 @@ let interp_ltac_var coerce ist env locid =
 (* Interprets an identifier which must be fresh *)
 let coerce_to_ident fresh env = function
   | VIntroPattern (IntroIdentifier id) -> id
-  | VConstr c when isVar c & not (fresh & is_variable env (destVar c)) ->
+  | VConstr ([],c) when isVar c & not (fresh & is_variable env (destVar c)) ->
       (* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *)
       destVar c
   | v -> raise (CannotCoerceTo "a fresh identifier")
@@ -1060,7 +1064,7 @@ let interp_fresh_name ist env = function
 
 let coerce_to_intro_pattern env = function
   | VIntroPattern ipat -> ipat
-  | VConstr c when isVar c ->
+  | VConstr ([],c) when isVar c ->
       (* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
       (* but also in "destruct H as (H,H')" *)
       IntroIdentifier (destVar c)
@@ -1107,11 +1111,16 @@ let interp_int_or_var_list ist l =
 
 let constr_of_value env = function
   | VConstr csr -> csr
-  | VIntroPattern (IntroIdentifier id) -> constr_of_id env id
+  | VIntroPattern (IntroIdentifier id) -> ([],constr_of_id env id)
   | _ -> raise Not_found
 
+let closed_constr_of_value env v =
+  let ids,c = constr_of_value env v in
+  if ids <> [] then raise Not_found;
+  c
+
 let coerce_to_hyp env = function
-  | VConstr c when isVar c -> destVar c
+  | VConstr ([],c) when isVar c -> destVar c
   | VIntroPattern (IntroIdentifier id) when is_variable env id -> id
   | _ -> raise (CannotCoerceTo "a variable")
 
@@ -1154,7 +1163,7 @@ let interp_move_location ist gl = function
 (* Interprets a qualified name *)
 let coerce_to_reference env v =
   try match v with
-  | VConstr c -> global_of_constr c (* may raise Not_found *)
+  | VConstr ([],c) -> global_of_constr c (* may raise Not_found *)
   | _ -> raise Not_found
   with Not_found -> raise (CannotCoerceTo "a reference")
 
@@ -1166,7 +1175,7 @@ let interp_reference ist env = function
 let pf_interp_reference ist gl = interp_reference ist (pf_env gl)
 
 let coerce_to_inductive = function
-  | VConstr c when isInd c -> destInd c
+  | VConstr ([],c) when isInd c -> destInd c
   | _ -> raise (CannotCoerceTo "an inductive type")
 
 let interp_inductive ist = function
@@ -1175,8 +1184,8 @@ let interp_inductive ist = function
 
 let coerce_to_evaluable_ref env v =
   let ev = match v with
-    | VConstr c when isConst c -> EvalConstRef (destConst c)
-    | VConstr c when isVar c -> EvalVarRef (destVar c)
+    | VConstr ([],c) when isConst c -> EvalConstRef (destConst c)
+    | VConstr ([],c) when isVar c -> EvalVarRef (destVar c)
     | VIntroPattern (IntroIdentifier id) when List.mem id (ids_of_context env)
 	-> EvalVarRef id
     | _ -> raise (CannotCoerceTo "an evaluable reference")
@@ -1214,18 +1223,18 @@ let interp_clause ist gl { onhyps=ol; concl_occs=occs } =
 (* Interpretation of constructions *)
 
 (* Extract the constr list from lfun *)
-let rec constr_list_aux env = function
+let extract_ltac_constr_values ist env =
+  let rec aux = function
   | (id,v)::tl ->
-      let (l1,l2) = constr_list_aux env tl in
+      let (l1,l2) = aux tl in
       (try ((id,constr_of_value env v)::l1,l2)
        with Not_found ->
 	 let ido = match v with
 	   | VIntroPattern (IntroIdentifier id0) -> Some id0
 	   | _ -> None in
 	 (l1,(id,ido)::l2))
-  | [] -> ([],[])
-
-let constr_list ist env = constr_list_aux env ist.lfun
+  | [] -> ([],[]) in
+  aux ist.lfun
 
 (* Extract the identifier list from lfun: join all branches (what to do else?)*)
 let rec intropattern_ids (loc,pat) = match pat with
@@ -1259,20 +1268,6 @@ let interp_fresh_id ist env l =
 
 let pf_interp_fresh_id ist gl = interp_fresh_id ist (pf_env gl)
 
-(* To retype a list of key*constr with undefined key *)
-let retype_list sigma env lst =
-  List.fold_right (fun (x,csr) a ->
-    try (x,Retyping.get_judgment_of env sigma csr)::a with
-    | Anomaly _ -> a) lst []
-
-let extract_ltac_vars_data ist sigma env =
-  let (ltacvars,_ as vars) = constr_list ist env in
-  vars, retype_list sigma env ltacvars
-
-let extract_ltac_vars ist sigma env =
-  let (_,unbndltacvars),typs = extract_ltac_vars_data ist sigma env in
-  typs,unbndltacvars
-
 let implicit_tactic = ref None
 
 let declare_implicit_tactic tac = implicit_tactic := Some tac
@@ -1326,8 +1321,7 @@ let solve_remaining_evars fail_evar use_classes env initial_sigma evd c =
   !evdref,c
 
 let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma (c,ce) =
-  let (ltacvars,unbndltacvars as vars),typs =
-    extract_ltac_vars_data ist sigma env in
+  let (ltacvars,unbndltacvars as vars) = extract_ltac_constr_values ist env in
   let c = match ce with
   | None -> c
     (* If at toplevel (ce<>None), the error can be due to an incorrect
@@ -1339,8 +1333,7 @@ let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma
   in
   let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in
   let evd,c =
-    catch_error trace
-      (understand_ltac expand_evar sigma env (typs,unbndltacvars) kind) c in
+    catch_error trace (understand_ltac expand_evar sigma env vars kind) c in
   let evd,c =
     if expand_evar then
       solve_remaining_evars fail_evar use_classes env sigma evd c
@@ -1378,7 +1371,7 @@ let pf_interp_constr ist gl =
   interp_constr ist (pf_env gl) (project gl)
 
 let constr_list_of_VList env = function
-  | VList l -> List.map (constr_of_value env) l
+  | VList l -> List.map (closed_constr_of_value env) l
   | _ -> raise Not_found
 
 let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
@@ -1484,31 +1477,32 @@ let interp_constr_may_eval ist gl c =
     csr
   end
 
-let rec message_of_value = function
+let rec message_of_value gl = function
   | VVoid -> str "()"
   | VInteger n -> int n
   | VIntroPattern ipat -> pr_intro_pattern (dloc,ipat)
-  | VConstr_context c | VConstr c -> pr_constr c
+  | VConstr_context c -> pr_constr_env (pf_env gl) c
+  | VConstr c -> pr_constr_under_binders_env (pf_env gl) c
   | VRec _ | VRTactic _ | VFun _ -> str "<tactic>"
-  | VList l -> prlist_with_sep spc message_of_value l
+  | VList l -> prlist_with_sep spc (message_of_value gl) l
 
-let rec interp_message_token ist = function
+let rec interp_message_token ist gl = function
   | MsgString s -> str s
   | MsgInt n -> int n
   | MsgIdent (loc,id) ->
       let v =
 	try List.assoc id ist.lfun
 	with Not_found -> user_err_loc (loc,"",pr_id id ++ str" not found.") in
-      message_of_value v
+      message_of_value gl v
 
-let rec interp_message_nl ist = function
+let rec interp_message_nl ist gl = function
   | [] -> mt()
-  | l -> prlist_with_sep spc (interp_message_token ist) l ++ fnl()
+  | l -> prlist_with_sep spc (interp_message_token ist gl) l ++ fnl()
 
-let interp_message ist l =
+let interp_message ist gl l =
   (* Force evaluation of interp_message_token so that potential errors
      are raised now and not at printing time *)
-  prlist (fun x -> spc () ++ x) (List.map (interp_message_token ist) l)
+  prlist (fun x -> spc () ++ x) (List.map (interp_message_token ist gl) l)
 
 let intro_pattern_list_of_Vlist loc env = function
   | VList l -> List.map (fun a -> loc,coerce_to_intro_pattern env a) l
@@ -1625,7 +1619,7 @@ let interp_induction_arg ist gl sigma arg =
         match List.assoc id ist.lfun with
 	| VInteger n -> ElimOnAnonHyp n
 	| VIntroPattern (IntroIdentifier id) -> ElimOnIdent (loc,id)
-	| VConstr c -> ElimOnConstr (c,NoBindings)
+	| VConstr ([],c) -> ElimOnConstr (c,NoBindings)
 	| _ -> user_err_loc (loc,"",
 	      strbrk "Cannot coerce " ++ pr_id id ++
 	      strbrk " neither to a quantified hypothesis nor to a term.")
@@ -1663,8 +1657,7 @@ let eval_pattern lfun ist env sigma (_,pat as c) =
   if use_types then
     snd (interp_typed_pattern ist env sigma c)
   else
-    let lvar = List.map (fun (id,c) -> (id,lazy(snd (pattern_of_constr Evd.empty c)))) lfun in
-    instantiate_pattern lvar pat
+    instantiate_pattern lfun pat
 
 let read_pattern lfun ist env sigma = function
   | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c)
@@ -1710,18 +1703,22 @@ let is_match_catchable = function
 (* different instances of the same metavars is here modulo conversion... *)
 let verify_metas_coherence gl (ln1,lcm) (ln,lm) =
   let rec aux = function
-  | (num,csr)::tl ->
-    if (List.for_all (fun (a,b) -> a<>num or pf_conv_x gl b csr) lcm) then
-      (num,csr)::aux tl
-    else
-      raise Not_coherent_metas
+  | (id,(ctx,c) as x)::tl ->
+      if List.for_all
+	(fun (id',(ctx',c')) -> id'<>id or ctx = ctx' & pf_conv_x gl c' c) lcm
+      then
+	x :: aux tl
+      else
+	raise Not_coherent_metas
   | [] -> lcm in
   (ln@ln1,aux lm)
 
+let adjust (l,lc) = (l,List.map (fun (id,c) -> (id,([],c))) lc)
+
 (* Tries to match one hypothesis pattern with a list of hypotheses *)
 let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
   let get_id_couple id = function
-    | Name idpat -> [idpat,VConstr (mkVar id)]
+    | Name idpat -> [idpat,VConstr ([],mkVar id)]
     | Anonymous -> [] in
   let match_pat lmatch hyp pat =
     match pat with
@@ -1736,11 +1733,11 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
         let rec match_next_pattern find_next () =
           let (lmeta,ctxt,find_next') = find_next () in
           try
-            let lmeta = verify_metas_coherence gl lmatch lmeta in
+            let lmeta = verify_metas_coherence gl lmatch (adjust lmeta) in
             (give_context ctxt ic,lmeta,match_next_pattern find_next')
           with
             | Not_coherent_metas -> match_next_pattern find_next' () in
-        match_next_pattern(fun () -> match_subterm_gen b t hyp) () in
+        match_next_pattern (fun () -> match_subterm_gen b t hyp) () in
   let rec apply_one_mhyp_context_rec = function
     | (id,b,hyp as hd)::tl ->
 	(match patv with
@@ -1782,8 +1779,8 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
 
 (* misc *)
 
-let mk_constr_value ist gl c = VConstr (pf_interp_constr ist gl c)
-let mk_hyp_value ist gl c = VConstr (mkVar (interp_hyp ist gl c))
+let mk_constr_value ist gl c = VConstr ([],pf_interp_constr ist gl c)
+let mk_hyp_value ist gl c = VConstr ([],mkVar (interp_hyp ist gl c))
 let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c)
 
 let pack_sigma (sigma,c) = {it=c;sigma=sigma}
@@ -1826,8 +1823,8 @@ and eval_tactic ist = function
 	catch_error (push_trace(loc,call)ist.trace) tac gl
   | TacFun _ | TacLetIn _ -> assert false
   | TacMatchGoal _ | TacMatch _ -> assert false
-  | TacId s -> tclIDTAC_MESSAGE (interp_message_nl ist s)
-  | TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) (interp_message ist s)
+  | TacId s -> fun gl -> tclIDTAC_MESSAGE (interp_message_nl ist gl s) gl
+  | TacFail (n,s) -> fun gl -> tclFAIL (interp_int_or_var ist n) (interp_message ist gl s) gl
   | TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
   | TacAbstract (tac,ido) ->
       fun gl -> Tactics.tclABSTRACT
@@ -1877,7 +1874,7 @@ and interp_tacarg ist gl = function
   | Reference r -> interp_ltac_reference dloc false ist gl r
   | Integer n -> VInteger n
   | IntroPattern ipat -> VIntroPattern (snd (interp_intro_pattern ist gl ipat))
-  | ConstrMayEval c -> VConstr (interp_constr_may_eval ist gl c)
+  | ConstrMayEval c -> VConstr ([],interp_constr_may_eval ist gl c)
   | MetaIdArg (loc,_,id) -> assert false
   | TacCall (loc,r,[]) -> interp_ltac_reference loc true ist gl r
   | TacCall (loc,f,l) ->
@@ -1898,7 +1895,7 @@ and interp_tacarg ist gl = function
       else if tg = "value" then
         value_out t
       else if tg = "constr" then
-        VConstr (constr_out t)
+        VConstr ([],constr_out t)
       else
         anomaly_loc (dloc, "Tacinterp.val_interp",
           (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">"))
@@ -1992,7 +1989,7 @@ and interp_match_goal ist goal lz lr lmr =
     let rec match_next_pattern find_next () =
       let (lgoal,ctxt,find_next') = find_next () in
       let lctxt = give_context ctxt id in
-      try apply_hyps_context ist env lz goal mt lctxt lgoal mhyps hyps
+      try apply_hyps_context ist env lz goal mt lctxt (adjust lgoal) mhyps hyps
       with e when is_match_catchable e -> match_next_pattern find_next' () in
     match_next_pattern (fun () -> match_subterm_gen app c csr) () in
   let rec apply_match_goal ist env goal nrs lex lpt =
@@ -2033,7 +2030,8 @@ and interp_match_goal ist goal lz lr lmr =
 		       else mt()) ++ str"."))
     end in
     apply_match_goal ist env goal 0 lmr
-      (read_match_rule (fst (constr_list ist env)) ist env (project goal) lmr)
+      (read_match_rule (fst (extract_ltac_constr_values ist env))
+	ist env (project goal) lmr)
 
 (* Tries to match the hypotheses in a Match Context *)
 and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
@@ -2161,7 +2159,7 @@ and interp_match ist g lz constr lmr =
     let rec match_next_pattern find_next () =
       let (lmatch,ctxt,find_next') = find_next () in
       let lctxt = give_context ctxt id in
-      let lfun = extend_values_with_bindings lmatch (lctxt@ist.lfun) in
+      let lfun = extend_values_with_bindings (adjust lmatch) (lctxt@ist.lfun) in
       try eval_with_fail {ist with lfun=lfun} lz g mt
       with e when is_match_catchable e ->
         match_next_pattern find_next' () in
@@ -2202,7 +2200,7 @@ and interp_match ist g lz constr lmr =
         debugging_exception_step ist true e
           (fun () -> str "evaluation of the matched expression");
         raise e in
-  let ilr = read_match_rule (fst (constr_list ist (pf_env g))) ist (pf_env g) (project g) lmr in
+  let ilr = read_match_rule (fst (extract_ltac_constr_values ist (pf_env g))) ist (pf_env g) (project g) lmr in
   let res =
      try apply_match ist csr ilr with e ->
        debugging_exception_step ist true e (fun () -> str "match expression");
@@ -2223,11 +2221,13 @@ and interp_ltac_constr ist gl e =
     let cresult = constr_of_value (pf_env gl) result in
     debugging_step ist (fun () ->
       Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++
-      str " has value " ++ fnl() ++ print_constr_env (pf_env gl) cresult);
-    cresult
+      str " has value " ++ fnl() ++
+      pr_constr_under_binders_env (pf_env gl) cresult);
+    if fst cresult <> [] then raise Not_found;
+    snd cresult
   with Not_found ->
     errorlabstrm ""
-      (str "Must evaluate to a term" ++ fnl() ++
+      (str "Must evaluate to a closed term" ++ fnl() ++
 	  str "offending expression: " ++ fnl() ++
           Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++ str "this is a " ++
           (match result with
@@ -2454,15 +2454,15 @@ and interp_atomic ist gl tac =
     | VarArgType ->
         mk_hyp_value ist gl (out_gen globwit_var x)
     | RefArgType ->
-        VConstr (constr_of_global
+        VConstr ([],constr_of_global
           (pf_interp_reference ist gl (out_gen globwit_ref x)))
     | SortArgType ->
-        VConstr (mkSort (interp_sort (out_gen globwit_sort x)))
+        VConstr ([],mkSort (interp_sort (out_gen globwit_sort x)))
     | ConstrArgType ->
         mk_constr_value ist gl (out_gen globwit_constr x)
     | ConstrMayEvalArgType ->
 	VConstr
-          (interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x))
+          ([],interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x))
     | ExtraArgType s when tactic_genarg_level s <> None ->
           (* Special treatment of tactic arguments *)
 	val_interp ist gl
@@ -3020,7 +3020,7 @@ let tacticOut = function
 
 let _ = Auto.set_extern_interp
   (fun l ->
-    let l = List.map (fun (id,c) -> (id,VConstr c)) l in
+    let l = List.map (fun (id,c) -> (id,VConstr ([],c))) l in
     interp_tactic {lfun=l;avoid_ids=[];debug=get_debug(); trace=[]})
 let _ = Auto.set_extern_intern_tac
   (fun l ->
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 7c731e2b9..5fa9c220d 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -27,7 +27,7 @@ type value =
   | VVoid
   | VInteger of int
   | VIntroPattern of intro_pattern_expr
-  | VConstr of constr
+  | VConstr of Pattern.constr_under_binders
   | VConstr_context of constr
   | VList of value list
   | VRec of (identifier*value) list ref * glob_tactic_expr
@@ -39,8 +39,8 @@ and interp_sign =
     debug : debug_info;
     trace : ltac_trace }
 
-val extract_ltac_vars : interp_sign -> Evd.evar_map -> Environ.env ->
-  Pretyping.var_map * Pretyping.unbound_ltac_var_map
+val extract_ltac_constr_values : interp_sign -> Environ.env ->
+  Pretyping.ltac_var_map
 
 (** Transforms an id into a constr if possible *)
 val constr_of_id : Environ.env -> identifier -> constr
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 2bb225c66..ef0d62285 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -22,7 +22,7 @@ open Genarg
 
 let assoc_var s ist =
   match List.assoc (Names.id_of_string s) ist.lfun with
-    | VConstr c -> c
+    | VConstr ([],c) -> c
     | _ -> failwith "tauto: anomaly"
 
 (** Parametrization of tauto *)
@@ -114,8 +114,8 @@ let flatten_contravariant_conj ist =
   | Some (_,args) ->
       let i = List.length args in
       if not binary_mode || i = 2 then
-	let newtyp = valueIn (VConstr (List.fold_right mkArrow args c)) in
-	let hyp = valueIn (VConstr hyp) in
+	let newtyp = valueIn (VConstr ([],List.fold_right mkArrow args c)) in
+	let hyp = valueIn (VConstr ([],hyp)) in
 	let intros =
 	  iter_tac (List.map (fun _ -> <:tactic< intro >>) args)
 	  <:tactic< idtac >> in
@@ -149,9 +149,9 @@ let flatten_contravariant_disj ist =
   | Some (_,args) ->
       let i = List.length args in
       if not binary_mode || i = 2 then
-	let hyp = valueIn (VConstr hyp) in
+	let hyp = valueIn (VConstr ([],hyp)) in
 	iter_tac (list_map_i (fun i arg ->
-	  let typ = valueIn (VConstr (mkArrow arg c)) in
+	  let typ = valueIn (VConstr ([],mkArrow arg c)) in
 	  <:tactic<
             let typ := $typ in
             let hyp := $hyp in
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 09d21628b..dfa41c820 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -230,3 +230,16 @@ Section LtacLoopTest.
   Timeout 1 try f()().
   Abort.
 End LtacLoopTest.
+
+(* Test binding of open terms *)
+
+Ltac test_open_match z :=
+  match z with
+    (forall y x, ?h = 0) => assert (forall x y, h = x + y)
+  end.
+
+Goal True.
+test_open_match (forall z y, y + z  = 0).
+reflexivity.
+apply I.
+Qed.
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 8fcf15608..39c545589 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -822,14 +822,14 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
 		 | _ -> mt ())
        | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
 	   let filter =
-	     function (id,None) -> None | (id,Some id') -> Some(id,mkVar id') in
+	     function (id,None) -> None | (id,Some id') -> Some(id,([],mkVar id')) in
 	   let unboundvars = list_map_filter filter unboundvars in
 	   quote (pr_rawconstr_env (Global.env()) c) ++
 	     (if unboundvars <> [] or vars <> [] then
 		strbrk " (with " ++
 		  prlist_with_sep pr_coma
 		  (fun (id,c) ->
-		     pr_id id ++ str ":=" ++ Printer.pr_lconstr c)
+		     pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
 		  (List.rev vars @ unboundvars) ++ str ")"
 	      else mt())) ++
       (if n=2 then str " (repeated twice)"