From 4a7677505b65816a9dcedca6e5091b2beaa903c5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 22 May 2003 22:37:50 +0000
Subject: 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
---
 tactics/tacinterp.ml | 4 ++--
 1 file 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;
-- 
cgit v1.2.3