Quelques modifications autour du filtrage Ltac:

- Optimisation du filtrage sous-terme de Ltac (cf sub_match) pour le cas
  où c'est le n-ième sous-termes qui finalement réussit (passage à une
  complexité en n plutôt que n^2, via l'utilisation de continuations).
- Sémantique du filtrage: suppression dans sub_match de la recherche
  dans le type des let (puisque ce n'est pas cencé être une
  information utilisateur) mais rajout de la recherche dans le champ
  cast qui lui est utilisateur.
- Nouvelle fonctionnalité: récupération des noms des variables liantes
  filtrées (dans matches/sub_match) et utilisation de ces noms dans
  ltac (utile pour récupérer x dans "exists x, P x");



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

6 files changed, 300 insertions, 253 deletions

diff --git a/CHANGES b/CHANGES
index 8097ccd3f..4af8854ce 100644
--- a/CHANGES
+++ b/CHANGES
@@ -203,6 +203,9 @@ Tactic Language
   "let ... in ..." into a lazy one.
 - Patterns for hypotheses types in "match goal" are now interpreted in
   type_scope.
+- A bound variable whose name is not used elsewhere now serves as
+  metavariable in "match" and it gets instantiated by an identifier
+  (allow e.g. to extract the name of a statement like "exists x, P x").
 
 Tactics
 
diff --git a/lib/util.ml b/lib/util.ml
index ebade654e..2a60ad7b0 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -626,6 +626,10 @@ let rec list_remove_first a = function
   | b::l -> b::list_remove_first a l
   | [] -> raise Not_found
 
+let rec list_remove_assoc_in_triple x = function
+  | [] -> []
+  | (y,_,_ as z)::l -> if x = y then l else z::list_remove_assoc_in_triple x l
+
 let list_add_set x l = if List.mem x l then l else x::l
 
 let list_eq_set l1 l2 =
diff --git a/lib/util.mli b/lib/util.mli
index 7e351e270..a341fa5a2 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -137,6 +137,7 @@ val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
 val list_except : 'a -> 'a list -> 'a list
 val list_remove : 'a -> 'a list -> 'a list
 val list_remove_first : 'a -> 'a list -> 'a list
+val list_remove_assoc_in_triple : 'a -> ('a * 'b * 'c) list -> ('a * 'b * 'c) list
 val list_for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
 val list_sep_last : 'a list -> 'a * 'a list
 val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 516211350..6b3b4e175 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -44,15 +44,37 @@ open Pattern
 
  *)
 
+type bound_ident_map = (identifier * identifier) list
+
 exception PatternMatchingFailure
 
-let constrain (n,m) sigma =
-  if List.mem_assoc n sigma then
-    if eq_constr m (List.assoc n sigma) then sigma
+let constrain (n,m) (names,terms as subst) =
+  try
+    if eq_constr m (List.assoc n terms) then subst
     else raise PatternMatchingFailure
-  else 
-    (n,m)::sigma
-    
+  with
+      Not_found ->
+        if List.mem_assoc n names then
+          Flags.if_verbose Pp.warning
+              ("Collision between bound variable "^string_of_id n^
+                 " and a metavariable of same name.");
+        (names,(n,m)::terms)
+
+let add_binders na1 na2 (names,terms as subst) =
+  match na1, na2 with
+  | Name id1, Name id2 ->
+      if List.mem_assoc id1 names then
+        (Flags.if_verbose Pp.warning
+          ("Collision between bound variables of name"^string_of_id id1);
+         (names,terms))
+      else
+        (if List.mem_assoc id1 terms then
+            Flags.if_verbose Pp.warning
+              ("Collision between bound variable "^string_of_id id1^
+                  " and another bound variable of same name.");
+         ((id1,id2)::names,terms));
+  | _ -> subst
+
 let build_lambda toabstract stk (m : constr) = 
   let rec buildrec m p_0 p_1 = match p_0,p_1 with 
     | (_, []) -> m
@@ -77,7 +99,10 @@ let same_case_structure (_,cs1,ind,_) ci2 br1 br2 =
   | None -> cs1 = ci2.ci_cstr_nargs
 
 let matches_core convert allow_partial_app pat c = 
-  let rec sorec stk sigma p t =
+  let conv = match convert with
+    | None -> eq_constr
+    | Some (env,sigma) -> is_conv env sigma in
+  let rec sorec stk subst p t =
     let cT = strip_outer_cast t in
     match p,kind_of_term cT with
       | PSoApp (n,args),m ->
@@ -89,7 +114,7 @@ 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) sigma
+	    constrain (n,build_lambda relargs stk cT) subst
 	  else
 	    raise PatternMatchingFailure
 
@@ -97,66 +122,63 @@ let matches_core convert allow_partial_app pat c =
 	  let depth = List.length stk in
           if depth = 0 then
             (* Optimisation *)
-            constrain (n,cT) sigma
+            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) sigma
+	      constrain (n,lift (-depth) cT) subst
             else 
 	      raise PatternMatchingFailure
 
-      | PMeta None, m -> sigma
+      | PMeta None, m -> subst
 
-      | PRef (VarRef v1), Var v2 when v1 = v2 -> sigma
+      | PRef (VarRef v1), Var v2 when v1 = v2 -> subst
 
-      | PVar v1, Var v2 when v1 = v2 -> sigma
+      | PVar v1, Var v2 when v1 = v2 -> subst
 
-      | PRef ref, _ when constr_of_global ref = cT -> sigma
+      | PRef ref, _ when conv (constr_of_global ref) cT -> subst
 
-      | PRel n1, Rel n2 when n1 = n2 -> sigma
+      | PRel n1, Rel n2 when n1 = n2 -> subst
 
-      | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> sigma
+      | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> subst
 
-      | PSort (RType _), Sort (Type _) -> sigma
+      | PSort (RType _), Sort (Type _) -> subst
 
-      | PApp (p, [||]), _ -> sorec stk sigma p t
+      | PApp (p, [||]), _ -> sorec stk subst p t
 
       | PApp (PApp (h, a1), a2), _ ->
-          sorec stk sigma (PApp(h,Array.append a1 a2)) t
+          sorec stk subst (PApp(h,Array.append a1 a2)) t
 
       | PApp (PMeta (Some n),args1), App (c2,args2) when allow_partial_app ->
           let p = Array.length args2 - Array.length args1 in
           if p>=0 then
             let args21, args22 = array_chop p args2 in
-            let sigma =
+            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) sigma
+	        constrain (n,lift (-depth) c) subst
               else
 	        raise PatternMatchingFailure in
-            array_fold_left2 (sorec stk) sigma args1 args22
+            array_fold_left2 (sorec stk) subst args1 args22
           else raise PatternMatchingFailure
 
       | PApp (c1,arg1), App (c2,arg2) ->
-        (try array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2
+        (try array_fold_left2 (sorec stk) (sorec stk subst c1 c2) arg1 arg2
          with Invalid_argument _ -> raise PatternMatchingFailure)
 
       | PProd (na1,c1,d1), Prod(na2,c2,d2) ->
-	  sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2
+	  sorec ((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 stk sigma c1 c2) d1 d2
+	  sorec ((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 stk sigma c1 c2) d1 d2
-
-      | PRef (ConstRef _ as ref), _ when convert <> None ->
-	  let (env,evars) = Option.get convert in
-	  let c = constr_of_global ref in
-	  if is_conv env evars c cT then sigma
-	  else raise PatternMatchingFailure
+	  sorec ((na2,t2)::stk)
+            (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2
 
       | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
 	  let ctx,b2 = decompose_lam_n_assum ci.ci_cstr_nargs.(0) b2 in
@@ -167,140 +189,129 @@ let matches_core convert allow_partial_app pat c =
 	    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 b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
-  	    sorec s' (sorec s (sorec stk sigma a1 a2) b1 b2) b1' b2'
+  	    sorec s' (sorec s (sorec stk subst a1 a2) b1 b2) b1' b2'
           else
             raise PatternMatchingFailure
 
       | PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) ->
 	  if same_case_structure ci1 ci2 br1 br2 then
   	    array_fold_left2 (sorec stk) 
-	      (sorec stk (sorec stk sigma a1 a2) p1 p2) br1 br2
+	      (sorec stk (sorec stk subst a1 a2) p1 p2) br1 br2
           else
             raise PatternMatchingFailure
 
-      |	PFix c1, Fix _ when eq_constr (mkFix c1) cT -> sigma
-      |	PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> sigma
+      |	PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst
+      |	PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst
       | _ -> raise PatternMatchingFailure
 
-  in 
-  Sort.list (fun (a,_) (b,_) -> a<b) (sorec [] [] pat c)
+  in
+  let names,terms = sorec [] ([],[]) pat c in
+  (names,Sort.list (fun (a,_) (b,_) -> a<b) terms)
 
-let matches = matches_core None false
+let extended_matches = matches_core None false
 
-let pmatches = matches_core None true
+let matches c p = snd (matches_core None false c p)
 
-(* To skip to the next occurrence *)
-exception NextOccurrence of int
+let pmatches c p = snd (matches_core None true c p)
+
+let special_meta = (-1)
 
 (* Tells if it is an authorized occurrence and if the instance is closed *)
-let authorized_occ nocc mres =
-  if not (List.for_all (fun (_,c) -> closed0 c) (fst mres)) then
+let authorized_occ sigma mk_ctx next =
+  if not (List.for_all (fun (_,c) -> closed0 c) (snd sigma)) then
     raise PatternMatchingFailure;
-  if nocc = 0 then mres
-  else raise (NextOccurrence nocc)
-
-let special_meta = (-1)
+  sigma, mk_ctx (mkMeta special_meta), next
 
 (* Tries to match a subterm of [c] with [pat] *)
-let rec sub_match ?(partial_app=false) nocc pat c =
+let rec sub_match ?(partial_app=false) pat c =
+  let rec aux c mk_ctx next =
   match kind_of_term c with
   | Cast (c1,k,c2) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
+    (try authorized_occ (extended_matches pat c) mk_ctx next with
     | PatternMatchingFailure ->
-      let (lm,lc) = try_sub_match nocc pat [c1] in
-      (lm,mkCast (List.hd lc, k,c2))
-    | NextOccurrence nocc ->
-      let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in
-      (lm,mkCast (List.hd lc, k,c2)))
- | Lambda (x,c1,c2) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
+      let mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in
+      try_aux [c1] mk_ctx next)
+  | Lambda (x,c1,c2) ->
+    (try authorized_occ (extended_matches pat c) mk_ctx next with
     | PatternMatchingFailure ->
-      let (lm,lc) = try_sub_match nocc pat [c1;c2] in
-      (lm,mkLambda (x,List.hd lc,List.nth lc 1))
-    | NextOccurrence nocc ->
-      let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in
-      (lm,mkLambda (x,List.hd lc,List.nth lc 1)))
+      let mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in
+      try_aux [c1;c2] mk_ctx next)
   | Prod (x,c1,c2) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
+    (try authorized_occ (extended_matches pat c) mk_ctx next with
     | PatternMatchingFailure ->
-      let (lm,lc) = try_sub_match nocc pat [c1;c2] in
-      (lm,mkProd (x,List.hd lc,List.nth lc 1))
-    | NextOccurrence nocc ->
-      let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in
-      (lm,mkProd (x,List.hd lc,List.nth lc 1)))
-  | LetIn (x,c1,t2,c2) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
+      let mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in
+      try_aux [c1;c2] mk_ctx next)
+  | LetIn (x,c1,t1,c2) ->
+    (try authorized_occ (extended_matches pat c) mk_ctx next with
     | PatternMatchingFailure ->
-      let (lm,lc) = try_sub_match nocc pat [c1;t2;c2] in
-      (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2))
-    | NextOccurrence nocc ->
-      let (lm,lc) = try_sub_match (nocc - 1) pat [c1;t2;c2] in
-      (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2)))
+      let mk_ctx = function [c1;c2] -> mkLetIn (x,c1,t1,c2) | _ -> assert false
+      in try_aux [c1;c2] mk_ctx next)
   | App (c1,lc) ->
-      let rec aux nocc app args =
-	match args with
-	| [] -> 
-	    let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in
-	      (lm,mkApp (List.hd le, Array.of_list (List.tl le)))
-	| arg :: args ->
-	    let app = mkApp (app, [|arg|]) in
-	      try let (lm,ce) = sub_match nocc pat app in
-		    (lm,mkApp (ce, Array.of_list args))
-	      with NextOccurrence nocc ->
-		aux nocc app args
-      in
-	(try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
-	| PatternMatchingFailure ->
-	    if partial_app then
-	      aux nocc c1 (Array.to_list lc)
-	    else
-	      let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in
-		(lm,mkApp (List.hd le, Array.of_list (List.tl le)))
-	| NextOccurrence nocc ->
-	    if partial_app then
-	      aux nocc c1 (Array.to_list lc)
-	    else
-	      let (lm,le) = try_sub_match (nocc - 1) pat (c1::(Array.to_list lc)) in
-		(lm,mkApp (List.hd le, Array.of_list (List.tl le))))
+      (try authorized_occ (extended_matches pat c) mk_ctx next with
+      | PatternMatchingFailure ->
+          let topdown = true in
+	  if partial_app then
+            if topdown then
+              let lc1 = Array.sub lc 0 (Array.length lc - 1) in
+              let app = mkApp (c1,lc1) in
+              let mk_ctx = function 
+                | [app';c] -> mk_ctx (mkApp (app',[|c|]))
+                | _ -> assert false in
+	      try_aux [app;array_last lc] mk_ctx next
+            else
+              let rec aux2 app args next =
+                match args with
+                | [] ->
+                  let mk_ctx le =
+                    mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
+	          try_aux (c1::Array.to_list lc) mk_ctx next
+	        | arg :: args ->
+                  let app = mkApp (app,[|arg|]) in
+                  let next () = aux2 app args next in
+                  let mk_ctx ce = mk_ctx (mkApp (ce, Array.of_list args)) in
+                  aux app mk_ctx next in
+              aux2 c1 (Array.to_list lc) next
+          else
+            let mk_ctx le =
+              mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
+	    try_aux (c1::Array.to_list lc) mk_ctx next)
   | Case (ci,hd,c1,lc) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
+    (try authorized_occ (extended_matches pat c) mk_ctx next with
     | PatternMatchingFailure ->
-      let (lm,le) = try_sub_match nocc pat (c1::Array.to_list lc) in
-      (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le)))
-    | NextOccurrence nocc ->
-      let (lm,le) = try_sub_match (nocc - 1) pat (c1::Array.to_list lc) in
-      (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))))
+      let mk_ctx le = 
+        mk_ctx (mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))) in
+      try_aux (c1::Array.to_list lc) mk_ctx next)
   | Construct _ | Fix _ | Ind _|CoFix _ |Evar _|Const _
   | Rel _|Meta _|Var _|Sort _ ->
-    (try authorized_occ nocc ((matches pat c),mkMeta special_meta) with
-    | PatternMatchingFailure -> raise (NextOccurrence nocc)
-    | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1)))
-
-(* Tries [sub_match] for all terms in the list *)
-and try_sub_match nocc pat lc =
-  let rec try_sub_match_rec nocc pat lacc = function
-    | [] -> raise (NextOccurrence nocc)
-    | c::tl ->
-      (try 
-         let (lm,ce) = sub_match nocc pat c in
-         (lm,lacc@(ce::tl))
-       with
-      | NextOccurrence nocc -> try_sub_match_rec nocc pat (lacc@[c]) tl) in
-  try_sub_match_rec nocc pat [] lc
-
-let match_subterm nocc pat c =
-  try sub_match nocc pat c
-  with NextOccurrence _ -> raise PatternMatchingFailure
-
-let match_appsubterm nocc pat c =
-  try sub_match ~partial_app:true nocc pat c
-  with NextOccurrence _ -> raise PatternMatchingFailure
+    (try authorized_occ (extended_matches pat c) mk_ctx next with
+    | PatternMatchingFailure -> next ())
+
+  (* Tries [sub_match] for all terms in the list *)
+  and try_aux lc mk_ctx next =
+    let rec try_sub_match_rec lacc = function
+      | [] -> next ()
+      | c::tl ->
+          let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in
+          let next () = try_sub_match_rec (c::lacc) tl in
+          aux c mk_ctx next in
+    try_sub_match_rec [] lc in
+  aux c (fun x -> x) (fun () -> raise PatternMatchingFailure)
+
+type subterm_matching_result =
+    (bound_ident_map * patvar_map) * constr * (unit -> subterm_matching_result)
+
+let match_subterm pat c = sub_match pat c
+
+let match_appsubterm pat c = sub_match ~partial_app:true pat c
+
+let match_subterm_gen app pat c = sub_match ~partial_app:app pat c
 
 let is_matching pat n =
   try let _ = matches pat n in true
   with PatternMatchingFailure -> false
 
-let matches_conv env sigma = matches_core (Some (env,sigma)) false
+let matches_conv env sigma c p =
+  snd (matches_core (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 42f9eab12..574a4bbd2 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -22,36 +22,54 @@ exception PatternMatchingFailure
 
 val special_meta : metavariable
 
+type bound_ident_map = (identifier * identifier) list
+
 (* [matches pat c] matches [c] against [pat] and returns the resulting
    assignment of metavariables; it raises [PatternMatchingFailure] if
    not matchable; bindings are given in increasing order based on the
    numbers given in the pattern *)
 val matches : constr_pattern -> constr -> patvar_map
 
-(* [is_matching pat c] just tells if [c] matches against [pat] *)
+(* [extended_matches pat c] also returns the names of bound variables
+   in [c] that matches the bound variables in [pat]; if several bound
+   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
 
+(* [is_matching pat c] just tells if [c] matches against [pat] *)
 val is_matching : constr_pattern -> constr -> bool
 
 (* [matches_conv env sigma] matches up to conversion in environment
    [(env,sigma)] when constants in pattern are concerned; it raises
    [PatternMatchingFailure] if not matchable; bindings are given in
    increasing order based on the numbers given in the pattern *)
-
 val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
 
+(* The type of subterm matching results: a substitution + a context
+   (whose hole is denoted with [special_meta]) + a continuation that
+   either returns the next matching subterm or raise PatternMatchingFailure *)
+type subterm_matching_result =
+    (bound_ident_map * patvar_map) * constr * (unit -> subterm_matching_result)
+
 (* [match_subterm n pat c] returns the substitution and the context
-   corresponding to the [n+1]th **closed** subterm of [c] matching [pat];
-   It raises PatternMatchingFailure if no such matching exists *)
-val match_subterm : int -> constr_pattern -> constr -> patvar_map * constr
+   corresponding to the first **closed** subterm of [c] matching [pat], and
+   a continuation that looks for the next matching subterm.
+   It raises PatternMatchingFailure if no subterm matches the pattern *)
+val match_subterm : constr_pattern -> constr -> subterm_matching_result
+
+(* [match_appsubterm pat c] returns the substitution and the context
+   corresponding to the first **closed** subterm of [c] matching [pat], 
+   considering application contexts as well. It also returns a
+   continuation that looks for the next matching subterm.
+   It raises PatternMatchingFailure if no subterm matches the pattern *)
+val match_appsubterm : constr_pattern -> constr -> subterm_matching_result
 
-(* [match_appsubterm n pat c] returns the substitution and the context
-   corresponding to the [n+1]th **closed** subterm of [c] matching [pat], 
-   considering application contexts as well;
-   It raises PatternMatchingFailure if no such matching exists *)
-val match_appsubterm : int -> constr_pattern -> constr -> patvar_map * constr
+(* [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *)
+val match_subterm_gen : bool (* true = with app context *) -> 
+   constr_pattern -> constr -> subterm_matching_result
 
 (* [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
    up to conversion for constants in patterns *)
-
 val is_matching_conv :
   env -> Evd.evar_map -> constr_pattern -> constr -> bool
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 897c8fd98..fc3673e6f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -649,6 +649,15 @@ let extern_request ch req gl la =
   List.iter (pf_apply (extern_tacarg ch) gl) la;
   output_string ch "</REQUEST>\n"
 
+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
+  (* For compatibility, bound variables are visible only if no other
+     binding of the same name exists *)
+  lmatch@lfun@lnames
+
 (* Reads the hypotheses of a Match Context rule *)
 let rec intern_match_context_hyps sigma env lfun = function
   | (Hyp ((_,na) as locna,mp))::tl ->
@@ -1042,77 +1051,79 @@ let is_match_catchable = function
   | e -> Logic.catchable_exception e
 
 (* Verifies if the matched list is coherent with respect to lcm *)
-let rec verify_metas_coherence gl lcm = function
+(* While non-linear matching is modulo eq_constr in matches, merge of *)
+(* 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)::(verify_metas_coherence gl lcm tl)
+      (num,csr)::aux tl
     else
       raise Not_coherent_metas
-  | [] -> []
-
-type match_result = 
-  | Matches of (Names.identifier * value) list * (Rawterm.patvar * Term.constr) list *
-      (int * bool)
-  | Fail of int * bool
+  | [] -> lcm in
+  (ln@ln1,aux lm)
 
 (* Tries to match one hypothesis pattern with a list of hypotheses *)
-let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) (lhyps,nocc) =
+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)]
     | Anonymous -> [] in
-  let match_pat lmatch nocc id hyp pat =
+  let match_pat lmatch hyp pat =
     match pat with
     | Term t ->
+        let lmeta = extended_matches t hyp in
         (try
-            let lmeta = verify_metas_coherence gl lmatch (matches t hyp) in
-              Matches ([],lmeta,(0, true))
+            let lmeta = verify_metas_coherence gl lmatch lmeta in
+            ([],lmeta,(fun () -> raise PatternMatchingFailure))
           with
-	  | PatternMatchingFailure | Not_coherent_metas ->
-              Fail (0, true))
+            | Not_coherent_metas -> raise PatternMatchingFailure);
     | Subterm (b,ic,t) ->
-        (try
-          let (lm,ctxt) = 
-	    if b then match_appsubterm nocc t hyp else match_subterm nocc t hyp 
-	  in
-          let lmeta = verify_metas_coherence gl lmatch lm in
-            Matches 
-	      (give_context ctxt ic,lmeta,(nocc + 1,false))
+        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
+            (give_context ctxt ic,lmeta,match_next_pattern find_next')
           with
-          | PatternMatchingFailure ->
-	      Fail (0, true)
-          | Not_coherent_metas ->
-              Fail (nocc + 1, false))
-  in
-  let rec apply_one_mhyp_context_rec nocc = function
-    | (id,b,hyp as hd)::tl as hyps ->
+            | Not_coherent_metas -> match_next_pattern find_next' () 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
-	| None -> 
-	    (match match_pat lmatch nocc id hyp pat with
-	    | Matches (ids, lmeta, (nocc, cont)) ->
-		(get_id_couple id hypname@ids,
-		lmeta,hd,((if cont then tl else hyps),nocc))
-	    | Fail (nocc, cont) ->
-		apply_one_mhyp_context_rec nocc (if cont then tl else hyps))
+	| None ->
+            let rec match_next_pattern find_next () =
+              try
+                let (ids, lmeta, find_next') = find_next () in
+		(get_id_couple id hypname@ids, lmeta, hd, 
+                 match_next_pattern find_next')
+              with
+                | PatternMatchingFailure -> apply_one_mhyp_context_rec tl in
+            match_next_pattern (fun () -> match_pat lmatch hyp pat) ()
 	| Some patv -> 
-	    (match b with
+	    match b with
 	    | Some body -> 
-		(match match_pat lmatch nocc id body patv with
-		| Matches (ids, lmeta, (noccv, cont)) ->
-		    (match match_pat (lmatch@lmeta) nocc id hyp pat with
-		    | Matches (ids', lmeta', (nocc', cont')) ->
-			(get_id_couple id hypname@ids@ids',
-			lmeta@lmeta',hd,((if cont || cont' then tl else hyps),nocc'))
-		    | Fail (nocc, cont) ->
-			apply_one_mhyp_context_rec nocc (if cont then tl else hyps))
-		| Fail (nocc, cont) ->
-		    apply_one_mhyp_context_rec nocc (if cont then tl else hyps))
-	    | None -> 
-		apply_one_mhyp_context_rec nocc tl))
+                let rec match_next_pattern_in_body next_in_body () =
+                  try
+                    let (ids,lmeta,next_in_body') = next_in_body() in
+                    let rec match_next_pattern_in_typ next_in_typ () =
+                      try
+                        let (ids',lmeta',next_in_typ') = next_in_typ() in
+		        (get_id_couple id hypname@ids@ids', lmeta', hd, 
+                         match_next_pattern_in_typ next_in_typ')
+                      with
+                        | PatternMatchingFailure ->
+                            match_next_pattern_in_body next_in_body' () in
+                    match_next_pattern_in_typ 
+                      (fun () -> match_pat lmeta hyp pat) ()
+                  with PatternMatchingFailure -> apply_one_mhyp_context_rec tl
+                in
+                match_next_pattern_in_body 
+                  (fun () -> match_pat lmatch body patv) ()
+            | None -> apply_one_mhyp_context_rec tl)
     | [] ->
         db_hyp_pattern_failure ist.debug env (hypname,pat);
         raise PatternMatchingFailure
   in
-    apply_one_mhyp_context_rec nocc lhyps
+    apply_one_mhyp_context_rec lhyps
 
 let constr_to_id loc = function
   | VConstr c when isVar c -> destVar c
@@ -1861,14 +1872,18 @@ and interp_letin ist gl llc u =
   val_interp ist gl u
 
 (* Interprets the Match Context expressions *)
-and interp_match_context ist g lz lr lmr =
-  let rec apply_goal_sub app ist env goal nocc (id,c) csr mt mhyps hyps =
-    let (lgoal,ctxt) = if app then match_appsubterm nocc c csr
-      else match_subterm nocc c csr in
-    let lctxt = give_context ctxt id in
+and interp_match_context ist goal lz lr lmr =
+  let hyps = pf_hyps goal in
+  let hyps = if lr then List.rev hyps else hyps in
+  let concl = pf_concl goal in
+  let env = pf_env goal in
+  let rec apply_goal_sub app ist (id,c) csr mt mhyps hyps =
+    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
-      with e when is_match_catchable e ->
-	apply_goal_sub app ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in
+      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_context ist env goal nrs lex lpt = 
     begin
       if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex);
@@ -1881,27 +1896,24 @@ and interp_match_context ist g lz lr lmr =
 		apply_match_context ist env goal (nrs+1) (List.tl lex) tl
 	    end
 	| (Pat (mhyps,mgoal,mt))::tl ->
-	    let hyps = pf_hyps goal in
-	    let hyps = if lr then List.rev hyps else hyps in
-	    let mhyps = List.rev mhyps (* Sens naturel *) in
-	    let concl = pf_concl goal in
-	      (match mgoal with
-		 | Term mg ->
-		     (try
-			let lgoal = matches mg concl in
-			  db_matched_concl ist.debug (pf_env goal) concl;
-			  apply_hyps_context ist env lz goal mt [] lgoal mhyps hyps
-		      with e when is_match_catchable e ->
-			(match e with
-			   | PatternMatchingFailure -> db_matching_failure ist.debug
-			   | Eval_fail s -> db_eval_failure ist.debug s
-			   | _ -> db_logic_failure ist.debug e);
-			apply_match_context ist env goal (nrs+1) (List.tl lex) tl)
-		 | Subterm (b,id,mg) ->
-		     (try apply_goal_sub b ist env goal 0 (id,mg) concl mt mhyps hyps
-		      with
-			| PatternMatchingFailure ->
-			    apply_match_context ist env goal (nrs+1) (List.tl lex) tl))
+            let mhyps = List.rev mhyps (* Sens naturel *) in
+	    (match mgoal with
+             | Term mg ->
+		 (try
+		     let lmatch = extended_matches mg concl in
+		     db_matched_concl ist.debug env concl;
+		     apply_hyps_context ist env lz goal mt [] lmatch mhyps hyps
+		   with e when is_match_catchable e ->
+		     (match e with
+		       | PatternMatchingFailure -> db_matching_failure ist.debug
+		       | Eval_fail s -> db_eval_failure ist.debug s
+		       | _ -> db_logic_failure ist.debug e);
+		     apply_match_context ist env goal (nrs+1) (List.tl lex) tl)
+	     | Subterm (b,id,mg) ->
+		 (try apply_goal_sub b ist (id,mg) concl mt mhyps hyps
+		   with
+		     | PatternMatchingFailure ->
+			 apply_match_context ist env goal (nrs+1) (List.tl lex) tl))
 	| _ ->
 	    errorlabstrm "Tacinterp.apply_match_context"
               (v 0 (str "No matching clauses for match goal" ++
@@ -1909,36 +1921,36 @@ and interp_match_context ist g lz lr lmr =
 			 fnl() ++ str "(use \"Set Ltac Debug\" for more info)"
 		       else mt())))
     end in
-  let env = pf_env g in
-    apply_match_context ist env g 0 lmr
+    apply_match_context ist env goal 0 lmr
       (read_match_rule (fst (constr_list ist env)) lmr)
 
 (* Tries to match the hypotheses in a Match Context *)
 and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
-  let rec apply_hyps_context_rec lfun lmatch lhyps_rest current = function
-    | hyp::tl as mhyps ->
-	let (hypname, mbod, mhyp) = 
-	  match hyp with
-	  | Hyp ((_,hypname),mhyp) -> hypname, None, mhyp
+  let rec apply_hyps_context_rec lfun lmatch lhyps_rest = function
+    | hyp_pat::tl ->
+	let (hypname, _, _ as hyp_pat) =
+	  match hyp_pat with
+	  | Hyp ((_,hypname),mhyp) -> hypname,  None, mhyp
 	  | Def ((_,hypname),mbod,mhyp) -> hypname, Some mbod, mhyp
 	in
-        let (lids,lm,hyp_match,next) =
-          apply_one_mhyp_context ist env goal lmatch (hypname,mbod,mhyp) current in
-        db_matched_hyp ist.debug (pf_env goal) hyp_match hypname;
-        begin 
+        let rec match_next_pattern find_next =
+          let (lids,lm,hyp_match,find_next') = find_next () in
+          db_matched_hyp ist.debug (pf_env goal) hyp_match hypname;
 	  try
-            let nextlhyps = list_except hyp_match lhyps_rest in
-            apply_hyps_context_rec (lfun@lids) (lmatch@lm) nextlhyps
-	      (nextlhyps,0) tl
+            let id_match = pi1 hyp_match in
+            let nextlhyps = list_remove_assoc_in_triple id_match lhyps_rest in
+            apply_hyps_context_rec (lfun@lids) lm nextlhyps tl
           with e when is_match_catchable e -> 
-	      apply_hyps_context_rec lfun lmatch lhyps_rest next mhyps
-        end
+	    match_next_pattern find_next' in
+        let init_match_pattern () =
+          apply_one_mhyp_context ist env goal lmatch hyp_pat lhyps_rest in
+        match_next_pattern init_match_pattern
     | [] ->
-	let lmatch = List.map (fun (id,c) -> (id,VConstr c)) lmatch in
+        let lfun = extend_values_with_bindings lmatch (lfun@ist.lfun) in
         db_mc_pattern_success ist.debug;
-        eval_with_fail {ist with lfun=lmatch@lfun@ist.lfun} lz goal mt
+        eval_with_fail {ist with lfun=lfun} lz goal mt
   in
-  apply_hyps_context_rec lctxt lgmatch hyps (hyps,0) mhyps
+  apply_hyps_context_rec lctxt lgmatch hyps mhyps
 
 and interp_external loc ist gl com req la =
   let f ch = extern_request ch req gl la in
@@ -2030,33 +2042,31 @@ and interp_genarg_var_list1 ist gl x =
 
 (* Interprets the Match expressions *)
 and interp_match ist g lz constr lmr =
-  let rec apply_match_subterm app ist nocc (id,c) csr mt =
-    let (lm,ctxt) = 
-      if app then match_appsubterm nocc c csr 
-      else match_subterm nocc c csr 
-    in
-    let lctxt = give_context ctxt id in
-    let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
-    try eval_with_fail {ist with lfun=lm@lctxt@ist.lfun} lz g mt
-    with e when is_match_catchable e ->
-      apply_match_subterm app ist (nocc + 1) (id,c) csr mt
-  in
+  let rec apply_match_subterm app ist (id,c) csr mt =
+    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
+      try eval_with_fail {ist with lfun=lfun} lz g mt
+      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 ist csr = function
     | (All t)::_ ->
         (try eval_with_fail ist lz g t
          with e when is_match_catchable e -> apply_match ist csr [])
     | (Pat ([],Term c,mt))::tl ->
         (try
-            let lm = 
-              try matches c csr
+            let lmatch = 
+              try extended_matches c csr
               with e ->
                 debugging_exception_step ist false e (fun () ->
                   str "matching with pattern" ++ fnl () ++
                   pr_constr_pattern_env (pf_env g) c);
                 raise e in
             try
-              let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
-              eval_with_fail { ist with lfun=lm@ist.lfun } lz g mt
+              let lfun = extend_values_with_bindings lmatch ist.lfun in
+              eval_with_fail { ist with lfun=lfun } lz g mt
             with e ->
               debugging_exception_step ist false e (fun () ->
                 str "rule body for pattern" ++
@@ -2067,7 +2077,7 @@ and interp_match ist g lz constr lmr =
            apply_match ist csr tl)
 
     | (Pat ([],Subterm (b,id,c),mt))::tl ->
-        (try apply_match_subterm b ist 0 (id,c) csr mt
+        (try apply_match_subterm b ist (id,c) csr mt
          with PatternMatchingFailure -> apply_match ist csr tl)
     | _ ->
       errorlabstrm "Tacinterp.apply_match" (str