Creating a dedicated ltac/ folder for Hightactics.

47 files changed, 12 insertions, 18 deletions

diff --git a/Makefile.build b/Makefile.build
index f4319243c..190a62d00 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -503,7 +503,7 @@ test-suite: world $(ALLSTDLIB).v
 ##################################################################
 
 .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping
-.PHONY: engine highparsing stm toplevel hightactics
+.PHONY: engine highparsing stm toplevel ltac
 
 lib: lib/clib.cma lib/lib.cma
 kernel: kernel/kernel.cma
@@ -518,7 +518,7 @@ pretyping: pretyping/pretyping.cma
 highparsing: parsing/highparsing.cma
 stm: stm/stm.cma
 toplevel: toplevel/toplevel.cma
-hightactics: tactics/hightactics.cma
+ltac: ltac/ltac.cma
 
 ###########################################################################
 # 2) theories and plugins files
@@ -869,7 +869,7 @@ parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d
 grammar/grammar.dot : | grammar/grammar.mllib.d
 	$(OCAMLDOC_MLLIBD)
 
-tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d
+tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d
 	$(OCAMLDOC_MLLIBD)
 
 %.dot: %.mli
diff --git a/Makefile.common b/Makefile.common
index 6cf332686..3e2bfcb3a 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	engine
+  toplevel	parsing	printing	grammar	        intf	engine	ltac
 
 PLUGINS:=\
   omega		romega 		micromega 	quote \
@@ -161,14 +161,14 @@ BYTERUN:=$(addprefix kernel/byterun/, \
   coq_fix_code.o coq_memory.o coq_values.o coq_interp.o )
 
 # LINK ORDER:
-# Beware that highparsing.cma should appear before hightactics.cma
+# Beware that highparsing.cma should appear before ltac.cma
 # respecting this order is useful for developers that want to load or link
 # the libraries directly
 
 CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.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
+	stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma ltac/ltac.cma
 
 TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
 
@@ -379,7 +379,7 @@ OCAMLDOCDIR=dev/ocamldoc
 DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \
 	./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \
 	./parsing/*.mli ./proofs/*.mli \
-	./tactics/*.mli ./stm/*.mli ./toplevel/*.mli)
+	./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.mli)
 
 # Defining options to generate dependencies graphs
 DOT=dot
diff --git a/dev/base_include b/dev/base_include
index 767e023ea..86f34b2ac 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -17,6 +17,7 @@
 #directory "grammar";;
 #directory "intf";;
 #directory "stm";;
+#directory "ltac";;
 
 #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
 #directory "+camlp5";; (* Gramext is found in top_printers.ml *)
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index fe896d316..00e7f5c53 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -19,13 +19,6 @@ highparsing :
  Files in parsing/ that cannot be linked too early.
  Contains the grammar rules g_*.ml4
 
-hightactics :
-
- Files in tactics/ that cannot be linked too early.
- These are the .ml4 files that uses the EXTEND possibilities
- provided by grammar.cma, for instance eauto.ml4.
-
-
 Special components
 ------------------
 
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index b00d084ed..f9310e076 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -20,7 +20,7 @@ exec $OCAMLDEBUG \
 	-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/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
         -I $COQTOP/plugins/cc         -I $COQTOP/plugins/dp \
         -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
         -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \
diff --git a/tactics/autorewrite.ml b/ltac/autorewrite.ml
index ea598b61c..ea598b61c 100644
--- a/tactics/autorewrite.ml
+++ b/ltac/autorewrite.ml
diff --git a/tactics/autorewrite.mli b/ltac/autorewrite.mli
index 6196b04e1..6196b04e1 100644
--- a/tactics/autorewrite.mli
+++ b/ltac/autorewrite.mli
diff --git a/tactics/class_tactics.ml b/ltac/class_tactics.ml
index 485559898..485559898 100644
--- a/tactics/class_tactics.ml
+++ b/ltac/class_tactics.ml
diff --git a/tactics/class_tactics.mli b/ltac/class_tactics.mli
index f1bcfa7dd..f1bcfa7dd 100644
--- a/tactics/class_tactics.mli
+++ b/ltac/class_tactics.mli
diff --git a/tactics/coretactics.ml4 b/ltac/coretactics.ml4
index 6c02a7202..6c02a7202 100644
--- a/tactics/coretactics.ml4
+++ b/ltac/coretactics.ml4
diff --git a/tactics/eauto.ml b/ltac/eauto.ml
index 044946759..044946759 100644
--- a/tactics/eauto.ml
+++ b/ltac/eauto.ml
diff --git a/tactics/eauto.mli b/ltac/eauto.mli
index 8812093d5..8812093d5 100644
--- a/tactics/eauto.mli
+++ b/ltac/eauto.mli
diff --git a/tactics/eqdecide.ml b/ltac/eqdecide.ml
index 7d0df2f52..7d0df2f52 100644
--- a/tactics/eqdecide.ml
+++ b/ltac/eqdecide.ml
diff --git a/tactics/eqdecide.mli b/ltac/eqdecide.mli
index cb48a5bcc..cb48a5bcc 100644
--- a/tactics/eqdecide.mli
+++ b/ltac/eqdecide.mli
diff --git a/tactics/evar_tactics.ml b/ltac/evar_tactics.ml
index 2e0996bf5..2e0996bf5 100644
--- a/tactics/evar_tactics.ml
+++ b/ltac/evar_tactics.ml
diff --git a/tactics/evar_tactics.mli b/ltac/evar_tactics.mli
index e67540c05..e67540c05 100644
--- a/tactics/evar_tactics.mli
+++ b/ltac/evar_tactics.mli
diff --git a/tactics/extraargs.ml4 b/ltac/extraargs.ml4
index d33ec91f9..d33ec91f9 100644
--- a/tactics/extraargs.ml4
+++ b/ltac/extraargs.ml4
diff --git a/tactics/extraargs.mli b/ltac/extraargs.mli
index 14aa69875..14aa69875 100644
--- a/tactics/extraargs.mli
+++ b/ltac/extraargs.mli
diff --git a/tactics/extratactics.ml4 b/ltac/extratactics.ml4
index 23aa8dcb4..23aa8dcb4 100644
--- a/tactics/extratactics.ml4
+++ b/ltac/extratactics.ml4
diff --git a/tactics/extratactics.mli b/ltac/extratactics.mli
index 18334dafe..18334dafe 100644
--- a/tactics/extratactics.mli
+++ b/ltac/extratactics.mli
diff --git a/tactics/g_auto.ml4 b/ltac/g_auto.ml4
index 788443944..788443944 100644
--- a/tactics/g_auto.ml4
+++ b/ltac/g_auto.ml4
diff --git a/tactics/g_class.ml4 b/ltac/g_class.ml4
index 9ef154541..9ef154541 100644
--- a/tactics/g_class.ml4
+++ b/ltac/g_class.ml4
diff --git a/tactics/g_eqdecide.ml4 b/ltac/g_eqdecide.ml4
index 905653281..905653281 100644
--- a/tactics/g_eqdecide.ml4
+++ b/ltac/g_eqdecide.ml4
diff --git a/tactics/g_ltac.ml4 b/ltac/g_ltac.ml4
index b55ac9ad0..b55ac9ad0 100644
--- a/tactics/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
diff --git a/tactics/g_obligations.ml4 b/ltac/g_obligations.ml4
index 4cd8bf1fe..4cd8bf1fe 100644
--- a/tactics/g_obligations.ml4
+++ b/ltac/g_obligations.ml4
diff --git a/tactics/g_rewrite.ml4 b/ltac/g_rewrite.ml4
index c4ef1f297..c4ef1f297 100644
--- a/tactics/g_rewrite.ml4
+++ b/ltac/g_rewrite.ml4
diff --git a/tactics/hightactics.mllib b/ltac/ltac.mllib
index 7987d774d..7987d774d 100644
--- a/tactics/hightactics.mllib
+++ b/ltac/ltac.mllib
diff --git a/tactics/rewrite.ml b/ltac/rewrite.ml
index fb04bee07..fb04bee07 100644
--- a/tactics/rewrite.ml
+++ b/ltac/rewrite.ml
diff --git a/tactics/rewrite.mli b/ltac/rewrite.mli
index 01709f29f..01709f29f 100644
--- a/tactics/rewrite.mli
+++ b/ltac/rewrite.mli
diff --git a/tactics/tacentries.ml b/ltac/tacentries.ml
index 711cd8d9d..711cd8d9d 100644
--- a/tactics/tacentries.ml
+++ b/ltac/tacentries.ml
diff --git a/tactics/tacentries.mli b/ltac/tacentries.mli
index 3cf0bc5cc..3cf0bc5cc 100644
--- a/tactics/tacentries.mli
+++ b/ltac/tacentries.mli
diff --git a/tactics/tacenv.ml b/ltac/tacenv.ml
index d2d3f3117..d2d3f3117 100644
--- a/tactics/tacenv.ml
+++ b/ltac/tacenv.ml
diff --git a/tactics/tacenv.mli b/ltac/tacenv.mli
index 88b54993b..88b54993b 100644
--- a/tactics/tacenv.mli
+++ b/ltac/tacenv.mli
diff --git a/tactics/tacintern.ml b/ltac/tacintern.ml
index a75805b4f..a75805b4f 100644
--- a/tactics/tacintern.ml
+++ b/ltac/tacintern.ml
diff --git a/tactics/tacintern.mli b/ltac/tacintern.mli
index 71ca354fa..71ca354fa 100644
--- a/tactics/tacintern.mli
+++ b/ltac/tacintern.mli
diff --git a/tactics/tacinterp.ml b/ltac/tacinterp.ml
index 4506f8159..4506f8159 100644
--- a/tactics/tacinterp.ml
+++ b/ltac/tacinterp.ml
diff --git a/tactics/tacinterp.mli b/ltac/tacinterp.mli
index 31327873e..31327873e 100644
--- a/tactics/tacinterp.mli
+++ b/ltac/tacinterp.mli
diff --git a/tactics/tacsubst.ml b/ltac/tacsubst.ml
index 4059877b7..4059877b7 100644
--- a/tactics/tacsubst.ml
+++ b/ltac/tacsubst.ml
diff --git a/tactics/tacsubst.mli b/ltac/tacsubst.mli
index c1bf27257..c1bf27257 100644
--- a/tactics/tacsubst.mli
+++ b/ltac/tacsubst.mli
diff --git a/tactics/tactic_debug.ml b/ltac/tactic_debug.ml
index d661f9677..d661f9677 100644
--- a/tactics/tactic_debug.ml
+++ b/ltac/tactic_debug.ml
diff --git a/tactics/tactic_debug.mli b/ltac/tactic_debug.mli
index 520fb41ef..520fb41ef 100644
--- a/tactics/tactic_debug.mli
+++ b/ltac/tactic_debug.mli
diff --git a/tactics/tactic_option.ml b/ltac/tactic_option.ml
index a5ba3b837..a5ba3b837 100644
--- a/tactics/tactic_option.ml
+++ b/ltac/tactic_option.ml
diff --git a/tactics/tactic_option.mli b/ltac/tactic_option.mli
index ed759a76d..ed759a76d 100644
--- a/tactics/tactic_option.mli
+++ b/ltac/tactic_option.mli
diff --git a/tactics/tauto.ml b/ltac/tauto.ml
index a86fdb98a..a86fdb98a 100644
--- a/tactics/tauto.ml
+++ b/ltac/tauto.ml
diff --git a/tactics/tauto.mli b/ltac/tauto.mli
index e69de29bb..e69de29bb 100644
--- a/tactics/tauto.mli
+++ b/ltac/tauto.mli
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 73ef7e1ed..ad1f8cbcc 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -107,7 +107,7 @@ let core_libs =
    "engine/engine"; "pretyping/pretyping"; "interp/interp";  "proofs/proofs";
    "parsing/parsing"; "printing/printing"; "tactics/tactics";
    "stm/stm"; "toplevel/toplevel";  "parsing/highparsing";
-   "tactics/hightactics"]
+   "ltac/ltac"]
 let core_cma = List.map (fun s -> s^".cma") core_libs
 let core_cmxa = List.map (fun s -> s^".cmxa") core_libs
 let core_mllib = List.map (fun s -> s^".mllib") core_libs
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 147759f5f..f1ad2c262 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -456,8 +456,8 @@ let variables is_install opt (args,defs) =
   -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\" \\
-  -I \"$(COQLIB)config\"";
+  -I \"$(COQLIB)toplevel\" -I \"$(COQLIB)ltac\" -I \"$(COQLIB)stm\" \\
+  -I \"$(COQLIB)grammar\" -I \"$(COQLIB)config\"";
     List.iter (fun c -> print " \\
   -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n";
     print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";