Correction due au changement de semantique de Match

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

2 files changed, 15 insertions, 13 deletions

diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index de8efbb39..5bc4e4433 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -207,31 +207,35 @@ Tactic Definition ApplyInverse mul FT lvar trm :=
 
 (**** Inverse test ****)
 
+Tactic Definition StrongFail tac := First [tac|Fail 2].
+
 Tactic Definition InverseTestAux FT trm :=
   Let AplusT = Eval Compute in (Aplus FT)
   And AmultT = Eval Compute in (Amult FT)
   And AoppT  = Eval Compute in (Aopp FT)
   And AinvT  = Eval Compute in (Ainv FT) In
   Match trm With
-  | [(AinvT ?)] -> Fail
-  | [(AoppT ?1)] -> (InverseTestAux FT ?1)
-  | [(AplusT ?1 ?2)] -> (InverseTestAux FT ?1);(InverseTestAux FT ?2)
-  | [(AmultT ?1 ?2)] -> (InverseTestAux FT ?1);(InverseTestAux FT ?2)
+  | [(AinvT ?)] -> Fail 1
+  | [(AoppT ?1)] -> StrongFail (InverseTestAux FT ?1)
+  | [(AplusT ?1 ?2)] ->
+    StrongFail ((InverseTestAux FT ?1);(InverseTestAux FT ?2))
+  | [(AmultT ?1 ?2)] ->
+    StrongFail ((InverseTestAux FT ?1);(InverseTestAux FT ?2))
   | _ -> Idtac.
 
 Tactic Definition InverseTest FT :=
   Let AplusT = Eval Compute in (Aplus FT) In
   Match Context With
-  | [|-?1== ?2] -> (InverseTestAux FT '(AplusT ?1 ?2)).
+  | [|- ?1==?2] -> (InverseTestAux FT '(AplusT ?1 ?2)).
 
 (**** Field itself ****)
 
 Tactic Definition ApplySimplif sfun :=
   (Match Context With
-   | [ |- (interp_ExprA ?1 ?2 ?3)==(interp_ExprA ? ? ?) ] ->
+   | [|- (interp_ExprA ?1 ?2 ?3)==(interp_ExprA ? ? ?)] ->
      (sfun ?1 ?2 ?3));
   (Match Context With
-   | [ |- (interp_ExprA ? ? ?)==(interp_ExprA ?1 ?2 ?3) ] ->
+   | [|- (interp_ExprA ? ? ?)==(interp_ExprA ?1 ?2 ?3)] ->
      (sfun ?1 ?2 ?3)).
 
 Tactic Definition Unfolds FT :=
@@ -257,4 +261,4 @@ Tactic Definition Field_Gen FT :=
      (Multiply mul);[(ApplySimplif ApplyMultiply);
        (ApplySimplif (ApplyInverse mul));
        (Let id = GrepMult In Clear id);Compute;
-       First [(InverseTest FT);Ring|(Field_Gen FT)]|Idtac]].
+       First [(InverseTest FT);Ring|Clear ft vm;(Field_Gen FT)]|Idtac]].
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 098c2568e..cb1fb9414 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -463,7 +463,6 @@ let set_debug pos = debug := pos
 (* Gives the state of debug *)
 let get_debug () = !debug
 
-
 (* Interprets any expression *)
 let rec val_interp ist ast =
 
@@ -899,10 +898,9 @@ and match_interp ist ast lmr =
     | _ ->
       errorlabstrm "Tacinterp.apply_match" [<'sTR
         "No matching clauses for Match">] in
-  let csr =
-    constr_of_Constr (unvarg (val_interp ist (List.hd lmr)))
-  and ilr = read_match_rule
-    ist.evc ist.env (constr_list ist.goalopt ist.lfun) (List.tl lmr) in
+  let csr = constr_of_Constr (unvarg (val_interp ist (List.hd lmr)))
+  and ilr = read_match_rule ist.evc ist.env (constr_list ist.goalopt ist.lfun)
+    (List.tl lmr) in
   apply_match ist csr ilr
 
 and tactic_interp ist ast g =