From 63e792e2cf320544bcd8b28b2e932b18d5f4af1f Mon Sep 17 00:00:00 2001
From: emakarov
Date: Thu, 22 Nov 2007 14:34:44 +0000
Subject: An update on Numbers. Added two files dealing with recursion, for
 information only.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10330 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Natural/Abstract/NPlusOrder.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/Numbers/Natural/Abstract/NPlusOrder.v')

diff --git a/theories/Numbers/Natural/Abstract/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NPlusOrder.v
index f459e8dd67..265ea81444 100644
--- a/theories/Numbers/Natural/Abstract/NPlusOrder.v
+++ b/theories/Numbers/Natural/Abstract/NPlusOrder.v
@@ -67,7 +67,7 @@ Proof NZplus_le_cases.
 Theorem plus_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m.
 Proof NZplus_pos_cases.
 
-(** Theorems true for natural numbers *)
+(* Theorems true for natural numbers *)
 
 Theorem le_plus_r : forall n m : N, n <= n + m.
 Proof.
@@ -111,4 +111,4 @@ do 2 rewrite <- plus_assoc in H4. do 2 apply <- plus_lt_mono_l in H4.
 now rewrite (plus_comm n' u), (plus_comm m' v).
 Qed.
 
-End NPlusOrderPropFunct.
\ No newline at end of file
+End NPlusOrderPropFunct.
-- 
cgit v1.2.3