diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-21 15:46:47 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-21 15:46:47 +0000 |
| commit | 469975942e7ce58127286e05adba06afe2fdd8e9 (patch) | |
| tree | 4ce6b2fa84cd0720cf225f848011214d78df6a0a /contrib | |
| parent | 41278f9af1a4db0682d619b7469ef8274f4437d4 (diff) | |
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
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/field/Field_Tactic.v | 20 |
1 files changed, 12 insertions, 8 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]]. |