diff options
| author | delahaye | 2002-03-19 03:33:38 +0000 |
|---|---|---|
| committer | delahaye | 2002-03-19 03:33:38 +0000 |
| commit | 0c690c0b517f8becbd0a61a68a43b30ea1da1380 (patch) | |
| tree | aab107d7d35555010ec1b5032c077d8b7bdafbe0 | |
| parent | c41b399c96092918797967c87430b6ee96b3dab4 (diff) | |
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
| -rw-r--r-- | contrib/field/Field_Tactic.v | 2 |
1 files changed, 1 insertions, 1 deletions
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)] -> |