diff options
| author | herbelin | 2003-05-22 22:37:50 +0000 |
|---|---|---|
| committer | herbelin | 2003-05-22 22:37:50 +0000 |
| commit | 4a7677505b65816a9dcedca6e5091b2beaa903c5 (patch) | |
| tree | 6178b10dd06fe6e7416b03b7e295d39e59c9af89 | |
| parent | 8314dd0de10732e4dd4a0feab3a4350ffd1f7e71 (diff) | |
Réparation d'un bug de backtracking qui lui-même succédait à une inefficacité
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4063 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 02e7e8fb4a..ddc5c3e3f7 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1432,9 +1432,9 @@ and match_context_interp ist g lr lmr = (read_match_rule (project g) env (fst (constr_list ist env)) lmr) (* Tries to match the hypotheses in a Match Context *) -and apply_hyps_context ist env goal mt (lgmatch:(Rawterm.patvar * Term.constr) list) mhyps hyps = +and apply_hyps_context ist env goal mt lgmatch mhyps hyps = let rec apply_hyps_context_rec lfun lmatch lhyps_rest current = function - | Hyp ((_,hypname),mhyp)::tl -> + | Hyp ((_,hypname),mhyp)::tl as mhyps -> let (lids,lm,hyp_match,next) = apply_one_mhyp_context ist env goal lmatch (hypname,mhyp) current in db_matched_hyp ist.debug (pf_env goal) hyp_match hypname; |