From 81a3634d0b72262fd8e6299bc94d9a7ab31ce3c0 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt
Date: Fri, 25 Oct 2019 01:01:10 +0900
Subject: editing documentation in order.v and ssrnum.v

---
 mathcomp/algebra/ssrnum.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'mathcomp/algebra')

diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 5737a2d..6bbf24a 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -6,7 +6,10 @@ From mathcomp Require Import ssralg poly.
 
 (******************************************************************************)
 (* This file defines some classes to manipulate number structures, i.e        *)
-(* structures with an order and a norm.                                       *)
+(* structures with an order and a norm. To use this file, insert              *)
+(* "Import Num.Theory." before your scripts. You can also "Import Num.Def."   *)
+(* to enjoy shorter notations (e.g., minr instead of Num.min, lerif instead   *)
+(* of Num.leif, etc.).                                                        *)
 (*                                                                            *)
 (*   * NumDomain (Integral domain with an order and a norm)                   *)
 (*    numDomainType == interface for a num integral domain.                   *)
-- 
cgit v1.2.3