diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | kernel/dune | 11 | ||||
| -rw-r--r-- | kernel/uint63_amd64_63.ml (renamed from kernel/uint63_amd64.ml) | 0 | ||||
| -rw-r--r-- | kernel/uint63_i386_31.ml (renamed from kernel/uint63_x86.ml) | 0 | ||||
| -rw-r--r-- | kernel/write_uint63.ml | 4 |
5 files changed, 6 insertions, 11 deletions
diff --git a/Makefile.build b/Makefile.build index 147668187f..c76c14f2de 100644 --- a/Makefile.build +++ b/Makefile.build @@ -365,7 +365,7 @@ $(COQPP): $(COQPPCMO) coqpp/coqpp_main.ml ########################################################################### # Specific rules for Uint63 ########################################################################### -kernel/uint63.ml: kernel/write_uint63.ml kernel/uint63_x86.ml kernel/uint63_amd64.ml +kernel/uint63.ml: kernel/write_uint63.ml kernel/uint63_i386_31.ml kernel/uint63_amd64_63.ml $(SHOW)'WRITE $@' $(HIDE)(cd kernel && ocaml unix.cma $(shell basename $<)) diff --git a/kernel/dune b/kernel/dune index 5b23a705ae..4038bf5638 100644 --- a/kernel/dune +++ b/kernel/dune @@ -3,7 +3,7 @@ (synopsis "The Coq Kernel") (public_name coq.kernel) (wrapped false) - (modules (:standard \ genOpcodeFiles uint63_x86 uint63_amd64 write_uint63)) + (modules (:standard \ genOpcodeFiles uint63_i386_31 uint63_amd64_63 write_uint63)) (libraries lib byterun dynlink)) (executable @@ -14,15 +14,10 @@ (targets copcodes.ml) (action (with-stdout-to %{targets} (run ./genOpcodeFiles.exe copml)))) -(executable - (name write_uint63) - (modules write_uint63) - (libraries unix)) - (rule (targets uint63.ml) - (deps (:gen ./write_uint63.exe) uint63_x86.ml uint63_amd64.ml) - (action (run %{gen}))) + (deps (:gen-file uint63_%{ocaml-config:architecture}_%{ocaml-config:int_size}.ml)) + (action (copy# %{gen-file} %{targets}))) (documentation (package coq)) diff --git a/kernel/uint63_amd64.ml b/kernel/uint63_amd64_63.ml index 2d4d685775..2d4d685775 100644 --- a/kernel/uint63_amd64.ml +++ b/kernel/uint63_amd64_63.ml diff --git a/kernel/uint63_x86.ml b/kernel/uint63_i386_31.ml index fa45c90241..fa45c90241 100644 --- a/kernel/uint63_x86.ml +++ b/kernel/uint63_i386_31.ml diff --git a/kernel/write_uint63.ml b/kernel/write_uint63.ml index beb59ce205..42bb5dfbb1 100644 --- a/kernel/write_uint63.ml +++ b/kernel/write_uint63.ml @@ -31,8 +31,8 @@ let ml_file_copy input output = let write_uint63 () = ml_file_copy - (if max_int = 1073741823 (* 32-bits *) then "uint63_x86.ml" - else (* 64 bits *) "uint63_amd64.ml") + (if max_int = 1073741823 (* 32-bits *) then "uint63_i386_31.ml" + else (* 64 bits *) "uint63_amd64_63.ml") "uint63.ml" let () = write_uint63 () |