diff options
| -rw-r--r-- | .merlin | 2 | ||||
| -rw-r--r-- | Makefile.build | 3 | ||||
| -rw-r--r-- | Makefile.common | 6 | ||||
| -rw-r--r-- | _tags | 1 | ||||
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | dev/ocamldebug-coq.run | 3 | ||||
| -rw-r--r-- | engine/engine.mllib | 4 | ||||
| -rw-r--r-- | engine/evd.ml (renamed from pretyping/evd.ml) | 0 | ||||
| -rw-r--r-- | engine/evd.mli (renamed from pretyping/evd.mli) | 0 | ||||
| -rw-r--r-- | engine/logic_monad.ml (renamed from proofs/logic_monad.ml) | 0 | ||||
| -rw-r--r-- | engine/logic_monad.mli (renamed from proofs/logic_monad.mli) | 0 | ||||
| -rw-r--r-- | engine/namegen.ml (renamed from pretyping/namegen.ml) | 0 | ||||
| -rw-r--r-- | engine/namegen.mli (renamed from pretyping/namegen.mli) | 0 | ||||
| -rw-r--r-- | engine/termops.ml (renamed from pretyping/termops.ml) | 0 | ||||
| -rw-r--r-- | engine/termops.mli (renamed from pretyping/termops.mli) | 0 | ||||
| -rw-r--r-- | myocamlbuild.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.mllib | 3 | ||||
| -rw-r--r-- | proofs/proofs.mllib | 1 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 2 |
20 files changed, 18 insertions, 12 deletions
@@ -12,6 +12,8 @@ S kernel/byterun B kernel/byterun S library B library +S engine +B engine S pretyping B pretyping S interp diff --git a/Makefile.build b/Makefile.build index a0f7879d5..0e3313ecc 100644 --- a/Makefile.build +++ b/Makefile.build @@ -501,12 +501,13 @@ test-suite: world $(ALLSTDLIB).v ################################################################## .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping -.PHONY: highparsing stm toplevel hightactics +.PHONY: engine highparsing stm toplevel hightactics lib: lib/clib.cma lib/lib.cma kernel: kernel/kernel.cma byterun: $(BYTERUN) library: library/library.cma +engine: engine/engine.cma proofs: proofs/proofs.cma tactics: tactics/tactics.cma interp: interp/interp.cma diff --git a/Makefile.common b/Makefile.common index 8c2f51467..16782650a 100644 --- a/Makefile.common +++ b/Makefile.common @@ -63,7 +63,7 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE) CORESRCDIRS:=\ config lib kernel kernel/byterun library \ proofs tactics pretyping interp stm \ - toplevel parsing printing grammar intf + toplevel parsing printing grammar intf engine PLUGINS:=\ omega romega micromega quote \ @@ -161,7 +161,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ # the libraries directly CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ - pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ + engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma \ stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma @@ -370,7 +370,7 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ OCAMLDOCDIR=dev/ocamldoc DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \ - ./pretyping/*.mli ./interp/*.mli printing/*.mli \ + ./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \ ./parsing/*.mli ./proofs/*.mli \ ./tactics/*.mli ./stm/*.mli ./toplevel/*.mli) @@ -63,6 +63,7 @@ "library": include "parsing": include "plugins": include +"engine": include "pretyping": include "printing": include "proofs": include diff --git a/dev/base_include b/dev/base_include index de63c557d..e086c64cd 100644 --- a/dev/base_include +++ b/dev/base_include @@ -8,6 +8,7 @@ #directory "toplevel";; #directory "library";; #directory "kernel";; +#directory "engine";; #directory "pretyping";; #directory "lib";; #directory "proofs";; diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index d4ab22ced..b00d084ed 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -17,7 +17,8 @@ exec $OCAMLDEBUG \ -I $COQTOP \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \ -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel \ - -I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \ + -I $COQTOP/library -I $COQTOP/engine \ + -I $COQTOP/pretyping -I $COQTOP/parsing \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \ -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ diff --git a/engine/engine.mllib b/engine/engine.mllib new file mode 100644 index 000000000..4073f7e44 --- /dev/null +++ b/engine/engine.mllib @@ -0,0 +1,4 @@ +Logic_monad +Termops +Namegen +Evd diff --git a/pretyping/evd.ml b/engine/evd.ml index 454c51195..454c51195 100644 --- a/pretyping/evd.ml +++ b/engine/evd.ml diff --git a/pretyping/evd.mli b/engine/evd.mli index 0765b951f..0765b951f 100644 --- a/pretyping/evd.mli +++ b/engine/evd.mli diff --git a/proofs/logic_monad.ml b/engine/logic_monad.ml index d509670ec..d509670ec 100644 --- a/proofs/logic_monad.ml +++ b/engine/logic_monad.ml diff --git a/proofs/logic_monad.mli b/engine/logic_monad.mli index ab729aff7..ab729aff7 100644 --- a/proofs/logic_monad.mli +++ b/engine/logic_monad.mli diff --git a/pretyping/namegen.ml b/engine/namegen.ml index 5aca11ae6..5aca11ae6 100644 --- a/pretyping/namegen.ml +++ b/engine/namegen.ml diff --git a/pretyping/namegen.mli b/engine/namegen.mli index f66bc6d88..f66bc6d88 100644 --- a/pretyping/namegen.mli +++ b/engine/namegen.mli diff --git a/pretyping/termops.ml b/engine/termops.ml index 9f04faa83..9f04faa83 100644 --- a/pretyping/termops.ml +++ b/engine/termops.ml diff --git a/pretyping/termops.mli b/engine/termops.mli index 2552c67e6..2552c67e6 100644 --- a/pretyping/termops.mli +++ b/engine/termops.mli diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 097a10425..73ef7e1ed 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -104,7 +104,7 @@ let _build = Options.build_dir let core_libs = ["lib/clib"; "lib/lib"; "kernel/kernel"; "library/library"; - "pretyping/pretyping"; "interp/interp"; "proofs/proofs"; + "engine/engine"; "pretyping/pretyping"; "interp/interp"; "proofs/proofs"; "parsing/parsing"; "printing/printing"; "tactics/tactics"; "stm/stm"; "toplevel/toplevel"; "parsing/highparsing"; "tactics/hightactics"] diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 25d17c7c9..436f61d7b 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,7 +1,4 @@ Locusops -Termops -Namegen -Evd Reductionops Vnorm Inductiveops diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 32bf5576f..de0879127 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -4,7 +4,6 @@ Evar_refiner Proof_using Proof_type Proof_errors -Logic_monad Proofview_monad Logic Proofview diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 84b4b5e5d..f9a84887d 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -442,7 +442,7 @@ let variables is_install opt (args,defs) = (* Caml executables and relative variables *) if !some_ml4file || !some_mlfile || !some_mlifile then begin print "COQSRCLIBS?=-I \"$(COQLIB)kernel\" -I \"$(COQLIB)lib\" \\ - -I \"$(COQLIB)library\" -I \"$(COQLIB)parsing\" -I \"$(COQLIB)pretyping\" \\ + -I \"$(COQLIB)library\" -I \"$(COQLIB)parsing\" -I \"$(COQLIB)engine\" -I \"$(COQLIB)pretyping\" \\ -I \"$(COQLIB)interp\" -I \"$(COQLIB)printing\" -I \"$(COQLIB)intf\" \\ -I \"$(COQLIB)proofs\" -I \"$(COQLIB)tactics\" -I \"$(COQLIB)tools\" \\ -I \"$(COQLIB)toplevel\" -I \"$(COQLIB)stm\" -I \"$(COQLIB)grammar\" \\ diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 03074ced7..1ce3fe28d 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -132,7 +132,7 @@ let init_ocaml_path () = Mltop.add_ml_dir (Envars.coqlib ()); List.iter add_subdir [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; - [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; + [ "engine" ]; [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; [ "tactics" ]; [ "toplevel" ]; [ "printing" ]; [ "intf" ]; [ "grammar" ]; [ "ide" ] ] |