diff options
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 217b26bbc4..e799c7b8be 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. |