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 02420c4d85..91dbc336be 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 a0f7879d53..0e3313ecc7 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 8c2f514674..16782650a7 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 5c978cabd2..f805eeaa3f 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 de63c557d3..e086c64cd9 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 d4ab22ced1..b00d084edb 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 0000000000..4073f7e44d
--- /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 454c51195b..454c51195b 100644
--- a/pretyping/evd.ml
+++ b/engine/evd.ml
diff --git a/pretyping/evd.mli b/engine/evd.mli
index 0765b951fd..0765b951fd 100644
--- a/pretyping/evd.mli
+++ b/engine/evd.mli
diff --git a/proofs/logic_monad.ml b/engine/logic_monad.ml
index d509670ec2..d509670ec2 100644
--- a/proofs/logic_monad.ml
+++ b/engine/logic_monad.ml
diff --git a/proofs/logic_monad.mli b/engine/logic_monad.mli
index ab729aff71..ab729aff71 100644
--- a/proofs/logic_monad.mli
+++ b/engine/logic_monad.mli
diff --git a/pretyping/namegen.ml b/engine/namegen.ml
index 5aca11ae61..5aca11ae61 100644
--- a/pretyping/namegen.ml
+++ b/engine/namegen.ml
diff --git a/pretyping/namegen.mli b/engine/namegen.mli
index f66bc6d88c..f66bc6d88c 100644
--- a/pretyping/namegen.mli
+++ b/engine/namegen.mli
diff --git a/pretyping/termops.ml b/engine/termops.ml
index 9f04faa839..9f04faa839 100644
--- a/pretyping/termops.ml
+++ b/engine/termops.ml
diff --git a/pretyping/termops.mli b/engine/termops.mli
index 2552c67e61..2552c67e61 100644
--- a/pretyping/termops.mli
+++ b/engine/termops.mli
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 097a104259..73ef7e1eda 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 25d17c7c9f..436f61d7b6 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 32bf5576fa..de08791272 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 84b4b5e5df..f9a84887d9 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 03074ced70..1ce3fe28da 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" ] ]