Integration of theories/Ints into theories/Numbers, again : better generation of NMake.v

 - genN.ml becomes NMake_gen.ml
 - no need to produce the corresponding binary: we use ocaml NMake_gen.ml > NMake.v 
 - beware! redoing a ./configure is mandatory after this commit



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10903 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 3 deletions

diff --git a/theories/Numbers/Natural/BigN/genN.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 2a6e4b16a..171c4ffed 100644
--- a/theories/Numbers/Natural/BigN/genN.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-(*S genN.ml : this file generates NMake.v *)
+(*S NMake_gen.ml : this file generates NMake.v *)
 
 
 (*s The two parameters that control the generation: *)
@@ -53,11 +53,13 @@ let _ =
   pr "(*         *       GNU Lesser General Public License Version 2.1        *)";
   pr "(************************************************************************)";
   pr "";
-  pr "(**";
+  pr "(** * NMake *)";
+  pr "";
+  pr "(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.";
   pr "- Authors: Benjamin Grégoire, Laurent Théry";
   pr "- Institution: INRIA";
   pr "- Date: 2007";
-  pr "- Remark: File automatically generated, DO NOT EDIT, see genN.ml instead";
+  pr "- Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT !";
   pr "*)";
   pr "";
   pr "Require Import BigNumPrelude.";