From a105bc07a504da50f4563793d31f34fa724b2bcb Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 4 Jun 2010 13:19:50 +0000
Subject: Extraction: finish ExtrOcamlNatInt, add similar translation
 nat==>big_int

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13074 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/extraction/ExtrOcamlBasic.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins/extraction/ExtrOcamlBasic.v')

diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v
index 1fcdfd655c..f01352212f 100644
--- a/plugins/extraction/ExtrOcamlBasic.v
+++ b/plugins/extraction/ExtrOcamlBasic.v
@@ -10,17 +10,17 @@
 
 Extract Inductive bool => bool [ true false ].
 Extract Inductive option => option [ Some None ].
-Extract Inductive prod => "( * )" [ "" ].
- (* The "" above is a hack, but produce nicer code than with "(,)" *)
 Extract Inductive unit => unit [ "()" ].
 Extract Inductive list => list [ "[]" "( :: )" ].
+Extract Inductive prod => "( * )" [ "" ].
 
-(** We could also map sumbool to bool, sumor to option, but
-    this isn't always a gain in clarity. We leave it to the user...
+(** NB: The "" above is a hack, but produce nicer code than "(,)" *)
+
+(** Mapping sumbool to bool and sumor to option is not always nicer,
+    but it helps when realizing stuff like [lt_eq_lt_dec] *)
 
 Extract Inductive sumbool => bool [ true false ].
 Extract Inductive sumor => option [ Some None ].
-*)
 
 (** Restore lazyness of andb, orb.
     NB: without these Extract Constant, andb/orb would be inlined
-- 
cgit v1.2.3