diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-26 13:59:13 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-26 13:59:13 +0000 |
commit | f6e1acbbe00aeb479fde229c3941e3a6a2d53068 (patch) | |
tree | ce3a6476de30cbf68c7668f5ecba92f457a721e8 /theories7/Reals/SplitRmult.v | |
parent | e0f9487be5ce770117a9c9c815af8c7010ff357b (diff) |
Suppression des fichiers .v en ancienne syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7733 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories7/Reals/SplitRmult.v')
-rw-r--r-- | theories7/Reals/SplitRmult.v | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/theories7/Reals/SplitRmult.v b/theories7/Reals/SplitRmult.v deleted file mode 100644 index e2a02fce4..000000000 --- a/theories7/Reals/SplitRmult.v +++ /dev/null @@ -1,19 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$ i*) - -(*i Lemma mult_non_zero :(r1,r2:R)``r1<>0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*) - - -Require Rbase. - -Recursive Tactic Definition SplitRmult := - Match Context With - | [ |- ~(Rmult ?1 ?2)==R0 ] -> Apply mult_non_zero; Split;Try SplitRmult. - |