diff options
Diffstat (limited to 'theories/QArith/Qreals.v')
| -rw-r--r-- | theories/QArith/Qreals.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 5b4d8db032..1b6b4722b4 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -11,7 +11,7 @@ Require Export Rbase. Require Export QArith_base. -(** * A field tactic for rational numbers. *) +(** A field tactic for rational numbers. *) (** Since field cannot operate on setoid datatypes (yet?), we translate Q goals into reals before applying field. *) |