diff options
| author | Florent Hivert | 2016-11-17 01:33:36 +0100 |
|---|---|---|
| committer | Florent Hivert | 2016-11-17 01:33:36 +0100 |
| commit | 84cc11db01159b17a8dcf4d02dbe0549067d228f (patch) | |
| tree | 964ee247bbf305022235217e716578a37be0bf62 /mathcomp/algebra/rat.v | |
| parent | 5daf14d44b9cd22c6b51b2b23b4eebe5f3aee79f (diff) | |
| parent | 23e57fb47874331c5feaace883513b7abecdff28 (diff) | |
Merge remote-tracking branch 'upstream/master' into fixdoc
Diffstat (limited to 'mathcomp/algebra/rat.v')
| -rw-r--r-- | mathcomp/algebra/rat.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 9012291..d004748 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -1,4 +1,4 @@ -(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp @@ -11,8 +11,6 @@ Require Import bigop ssralg div ssrnum ssrint. (* structure of archimedean, real field, with int and nat declared as closed *) (* subrings. *) (* rat == the type of rational number, with single constructor Rat *) -(* Rat p h == the element of type rat build from p a pair of integers and*) -(* h a proof of (0 < p.2) && coprime `|p.1| `|p.2| *) (* n%:Q == explicit cast from int to rat, postfix notation for the *) (* ratz constant *) (* numq r == numerator of (r : rat) *) |