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

1 files changed, 5 insertions, 5 deletions

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