From e539db48ab064dc0c10c5ebeb043372c840497c2 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Fri, 9 Mar 2018 15:23:17 +0100
Subject: Numeral Notation: minor text improvements suggested by J. Gross

---
 plugins/syntax/g_numeral.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
index 9edb7c3351..41d02adbe1 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -27,7 +27,7 @@ open Misctypes
     that starts with the right constructor, but might be partially
     applied.
 
-    At least [c] is known to be evar-free, since it comes for
+    At least [c] is known to be evar-free, since it comes from
     our own ad-hoc [constr_of_glob] or from conversions such
     as [coqint_of_rawnum].
 *)
@@ -65,7 +65,7 @@ let warning_abstract_num ty f =
 
 (** Comparing two raw numbers (base 10, big-endian, non-negative).
     A bit nasty, but not critical : only used to decide when a
-    nat number is considered as large. *)
+    number is considered as large (see warnings above). *)
 
 exception Comp of int
 
-- 
cgit v1.2.3