diff options
| author | jforest | 2010-05-06 09:33:08 +0000 |
|---|---|---|
| committer | jforest | 2010-05-06 09:33:08 +0000 |
| commit | 05656bc31bdc0c07d52321c9e5dbfd97ff2c25c2 (patch) | |
| tree | 5b1bc09cc6653d00231c08704c6bb036cd53a5eb | |
| parent | f95034fa6ec4341d980e0a9cf686764bd2866eec (diff) | |
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
| -rw-r--r-- | tactics/tacinterp.ml | 4 |
1 files 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 = |