diff options
| author |  mayero <mayero@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-24 19:56:29 +0000 |
|---|---|---|
| committer | mayero <mayero@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-24 19:56:29 +0000 |
| commit | 9e19a6257e14619eed8e60987a445c3afa57557b (patch) | |
| tree | 67701cbf53082916c71b38f7c9d2a3102e8a91a7 /theories/Reals/SplitRmult.v | |
| parent | ebf2a25f97c3ffc3376967d2841fbd681e6d69c2 (diff) | |
correction nom
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1702 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/SplitRmult.v')
| -rw-r--r-- | theories/Reals/SplitRmult.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/SplitRmult.v b/theories/Reals/SplitRmult.v index 217b26bbc..e799c7b8b 100644 --- a/theories/Reals/SplitRmult.v +++ b/theories/Reals/SplitRmult.v @@ -13,7 +13,7 @@ Require Rbase. -Tactic Definition SplitRMult := +Tactic Definition SplitRmult := Match Context With - | [ |- ~(Rmult ?1 ?2)==R0 ] -> Apply mult_non_zero; Split;Try SplitRMult. + | [ |- ~(Rmult ?1 ?2)==R0 ] -> Apply mult_non_zero; Split;Try SplitRmult. |