From 0c690c0b517f8becbd0a61a68a43b30ea1da1380 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Tue, 19 Mar 2002 03:33:38 +0000
Subject: Fix d'un bug sur le test des inverses

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2542 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/field/Field_Tactic.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index a18d87f0aa..7be170ebb7 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -221,7 +221,7 @@ Tactic Definition InverseTestAux FT trm :=
   And AinvT  = Eval Cbv Beta Delta [Ainv] Iota in (Ainv FT) In
   Match trm With
   | [(AinvT ?)] -> Fail 1
-  | [(AoppT ?1)] -> StrongFail (InverseTestAux FT ?1)
+  | [(AoppT ?1)] -> StrongFail ((InverseTestAux FT ?1);Idtac)
   | [(AplusT ?1 ?2)] ->
     StrongFail ((InverseTestAux FT ?1);(InverseTestAux FT ?2))
   | [(AmultT ?1 ?2)] ->
-- 
cgit v1.2.3