diff options
| author | herbelin | 2003-10-21 12:23:34 +0000 |
|---|---|---|
| committer | herbelin | 2003-10-21 12:23:34 +0000 |
| commit | baacd9ba5f71a4fc0ce95e226d6a10b689736c82 (patch) | |
| tree | ddd70cee3d4a919e2b78eb95d51ea12a16ad2ccd | |
| parent | 467e6faa8ead498c23b222c91890679902f16daf (diff) | |
Type relation dans Datatypes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4691 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/ZArith/fast_integer.v | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v index 203d158309..68d80e8905 100644 --- a/theories/ZArith/fast_integer.v +++ b/theories/ZArith/fast_integer.v @@ -177,18 +177,6 @@ V8Infix "*" times : positive_scope. (**********************************************************************) (** Comparison on binary positive numbers *) -Inductive relation : Set := - EGAL :relation | INFERIEUR : relation | SUPERIEUR : relation. - -Definition Op := [r:relation] - Cases r of - EGAL => EGAL - | INFERIEUR => SUPERIEUR - | SUPERIEUR => INFERIEUR - end. - -(** Comparison of binary positive numbers *) - Fixpoint compare [x,y:positive]: relation -> relation := [r:relation] Cases x y of |