From 6b9e7f66db123a27c5ac7c52bebc67580940bfb6 Mon Sep 17 00:00:00 2001
From: Florent Hivert
Date: Tue, 11 Sep 2018 19:35:26 +0200
Subject: Fixes the doc of rat

---
 mathcomp/algebra/rat.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index 27f59f5..b56bc2a 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -11,8 +11,8 @@ 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   *)
-(*         n%:Q == explicit cast from int to rat, postfix notation for the    *)
-(*                 ratz constant                                              *)
+(*         n%:Q == explicit cast from int to rat, ie. the specialization to   *)
+(*                 rationals of the generic ring morphism n%:~R               *)
 (*       numq r == numerator of (r : rat)                                     *)
 (*       denq r == denominator of (r : rat)                                   *)
 (* x \is a Qint == x is an element of rat whose denominator is equal to 1     *)
-- 
cgit v1.2.3