diff options
| -rw-r--r-- | Makefile | 5 | ||||
| -rw-r--r-- | Makefile.build | 9 | ||||
| -rw-r--r-- | config/Makefile.template | 1 | ||||
| -rwxr-xr-x | configure | 1 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml (renamed from theories/Numbers/Natural/BigN/genN.ml) | 8 |
5 files changed, 12 insertions, 12 deletions
@@ -33,7 +33,8 @@ export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \ scripts/tolink.ml kernel/copcodes.ml export GENMLIFILES:=$(YACCFILES:.mly=.mli) export GENHFILES:=kernel/byterun/coq_jumptbl.h -export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) +export GENVFILES:=theories/Numbers/Natural/BigN/NMake.v +export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) export MLFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml' ')' $(FIND_PRINTF_P) | \ while read f; do if ! [ -e "$${f}4" ]; then echo "$$f"; fi; done) \ $(GENMLFILES) @@ -154,7 +155,6 @@ indepclean: rm -f toplevel/mltop.byteml toplevel/mltop.optml rm -f glob.dump rm -f revision - rm -f theories/Numbers/Natural/BigN/NMake.v docclean: rm -f doc/*/*.dvi doc/*/*.aux doc/*/*.log doc/*/*.bbl doc/*/*.blg doc/*/*.toc \ @@ -180,7 +180,6 @@ archclean: clean-ide cleantheories find . -name '*.cmx' -or -name '*.cmxa' -or -name '*.[soa]' | xargs rm -f rm -f $(TOOLS) rm -f $(MINICOQ) - rm -f theories/Numbers/Natural/BigN/genN clean-ide: rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE) diff --git a/Makefile.build b/Makefile.build index 5536ea775..5e89e08fa 100644 --- a/Makefile.build +++ b/Makefile.build @@ -523,11 +523,8 @@ theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | $(HIDE)rm -f theories/Init/$*.glob $(HIDE)$(BOOTCOQTOP) -dump-glob theories/Init/$*.glob -nois -compile theories/Init/$* -theories/Numbers/Natural/BigN/genN: theories/Numbers/Natural/BigN/genN.ml - $(OCAMLC) -o $@ $< - -theories/Numbers/Natural/BigN/NMake.v: theories/Numbers/Natural/BigN/genN - $< > $@ +theories/Numbers/Natural/BigN/NMake.v: theories/Numbers/Natural/BigN/NMake_gen.ml + $(OCAML) $< > $@ ########################################################################### # tools @@ -853,7 +850,7 @@ endif $(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $@ \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) -%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEP) +%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEP) $(GENVFILES) $(SHOW)'COQDEP $<' $(HIDE)$(COQDEP) -glob -slash -boot $(COQINCLUDES) "$<" > "$@" \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) diff --git a/config/Makefile.template b/config/Makefile.template index 409e49467..f35af2b58 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -56,6 +56,7 @@ MYCAMLP4LIB="CAMLP4LIBDIRECTORY" COQIDEINCLUDES=LABLGTKINCLUDES # Objective-Caml compile command +OCAML="OCAMLEXEC" OCAMLC="BYTECAMLC" OCAMLOPT="NATIVECAMLC" OCAMLDEP="OCAMLDEPEXEC" @@ -890,6 +890,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|EXECUTEEXTENSION|$EXE|" \ -e "s|BYTECAMLC|$bytecamlc|" \ -e "s|NATIVECAMLC|$nativecamlc|" \ + -e "s|OCAMLEXEC|$ocamlexec|" \ -e "s|OCAMLDEPEXEC|$ocamldepexec|" \ -e "s|OCAMLDOCEXEC|$ocamldocexec|" \ -e "s|OCAMLLEXEXEC|$ocamllexexec|" \ 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."; |