From 05656bc31bdc0c07d52321c9e5dbfd97ff2c25c2 Mon Sep 17 00:00:00 2001
From: jforest
Date: Thu, 6 May 2010 09:33:08 +0000
Subject: term matching in ltac was not coherent with match goal in presence of
 wildcards (no backtrack  if the tactic failed).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12996 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 86bd7cbee8..90b3686f18 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2166,9 +2166,9 @@ and interp_match ist g lz constr lmr =
         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)::_ ->
+    | (All t)::tl ->
         (try eval_with_fail ist lz g t
-         with e when is_match_catchable e -> apply_match ist csr [])
+         with e when is_match_catchable e -> apply_match ist csr tl)
     | (Pat ([],Term c,mt))::tl ->
         (try
             let lmatch =
-- 
cgit v1.2.3