diff options
| -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 |