Adding a new folder corresponding to the low-level part of the pretyper

together with the tactic monad.

The move is not complete yet, because some file candidates for this directory
have almost useless dependencies in other ones that should not be moved.

20 files changed, 18 insertions, 12 deletions

diff --git a/.merlin b/.merlin
index 02420c4d8..91dbc336b 100644
--- a/.merlin
+++ b/.merlin
@@ -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)
 
diff --git a/_tags b/_tags
index 5c978cabd..f805eeaa3 100644
--- a/_tags
+++ b/_tags
@@ -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" ] ]