From 9e19a6257e14619eed8e60987a445c3afa57557b Mon Sep 17 00:00:00 2001
From: mayero
Date: Tue, 24 Apr 2001 19:56:29 +0000
Subject: correction nom

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1702 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/SplitRmult.v | 4 ++--
 1 file 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.
 
-- 
cgit v1.2.3