Creating a dedicated ltac/ folder for Hightactics.

47 files changed, 12 insertions, 18 deletions

diff --git a/Makefile.build b/Makefile.build
index f4319243c5..190a62d000 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 6cf332686d..3e2bfcb3aa 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 767e023ea2..86f34b2ac9 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 fe896d3160..00e7f5c53c 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 b00d084edb..f9310e076a 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 ea598b61ca..ea598b61ca 100644
--- a/tactics/autorewrite.ml
+++ b/ltac/autorewrite.ml
diff --git a/tactics/autorewrite.mli b/ltac/autorewrite.mli
index 6196b04e18..6196b04e18 100644
--- a/tactics/autorewrite.mli
+++ b/ltac/autorewrite.mli
diff --git a/tactics/class_tactics.ml b/ltac/class_tactics.ml
index 4855598989..4855598989 100644
--- a/tactics/class_tactics.ml
+++ b/ltac/class_tactics.ml
diff --git a/tactics/class_tactics.mli b/ltac/class_tactics.mli
index f1bcfa7dd4..f1bcfa7dd4 100644
--- a/tactics/class_tactics.mli
+++ b/ltac/class_tactics.mli
diff --git a/tactics/coretactics.ml4 b/ltac/coretactics.ml4
index 6c02a7202f..6c02a7202f 100644
--- a/tactics/coretactics.ml4
+++ b/ltac/coretactics.ml4
diff --git a/tactics/eauto.ml b/ltac/eauto.ml
index 0449467598..0449467598 100644
--- a/tactics/eauto.ml
+++ b/ltac/eauto.ml
diff --git a/tactics/eauto.mli b/ltac/eauto.mli
index 8812093d5f..8812093d5f 100644
--- a/tactics/eauto.mli
+++ b/ltac/eauto.mli
diff --git a/tactics/eqdecide.ml b/ltac/eqdecide.ml
index 7d0df2f522..7d0df2f522 100644
--- a/tactics/eqdecide.ml
+++ b/ltac/eqdecide.ml
diff --git a/tactics/eqdecide.mli b/ltac/eqdecide.mli
index cb48a5bcc8..cb48a5bcc8 100644
--- a/tactics/eqdecide.mli
+++ b/ltac/eqdecide.mli
diff --git a/tactics/evar_tactics.ml b/ltac/evar_tactics.ml
index 2e0996bf5a..2e0996bf5a 100644
--- a/tactics/evar_tactics.ml
+++ b/ltac/evar_tactics.ml
diff --git a/tactics/evar_tactics.mli b/ltac/evar_tactics.mli
index e67540c055..e67540c055 100644
--- a/tactics/evar_tactics.mli
+++ b/ltac/evar_tactics.mli
diff --git a/tactics/extraargs.ml4 b/ltac/extraargs.ml4
index d33ec91f9d..d33ec91f9d 100644
--- a/tactics/extraargs.ml4
+++ b/ltac/extraargs.ml4
diff --git a/tactics/extraargs.mli b/ltac/extraargs.mli
index 14aa69875f..14aa69875f 100644
--- a/tactics/extraargs.mli
+++ b/ltac/extraargs.mli
diff --git a/tactics/extratactics.ml4 b/ltac/extratactics.ml4
index 23aa8dcb47..23aa8dcb47 100644
--- a/tactics/extratactics.ml4
+++ b/ltac/extratactics.ml4
diff --git a/tactics/extratactics.mli b/ltac/extratactics.mli
index 18334dafe7..18334dafe7 100644
--- a/tactics/extratactics.mli
+++ b/ltac/extratactics.mli
diff --git a/tactics/g_auto.ml4 b/ltac/g_auto.ml4
index 788443944f..788443944f 100644
--- a/tactics/g_auto.ml4
+++ b/ltac/g_auto.ml4
diff --git a/tactics/g_class.ml4 b/ltac/g_class.ml4
index 9ef1545416..9ef1545416 100644
--- a/tactics/g_class.ml4
+++ b/ltac/g_class.ml4
diff --git a/tactics/g_eqdecide.ml4 b/ltac/g_eqdecide.ml4
index 905653281c..905653281c 100644
--- a/tactics/g_eqdecide.ml4
+++ b/ltac/g_eqdecide.ml4
diff --git a/tactics/g_ltac.ml4 b/ltac/g_ltac.ml4
index b55ac9ad06..b55ac9ad06 100644
--- a/tactics/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
diff --git a/tactics/g_obligations.ml4 b/ltac/g_obligations.ml4
index 4cd8bf1feb..4cd8bf1feb 100644
--- a/tactics/g_obligations.ml4
+++ b/ltac/g_obligations.ml4
diff --git a/tactics/g_rewrite.ml4 b/ltac/g_rewrite.ml4
index c4ef1f297e..c4ef1f297e 100644
--- a/tactics/g_rewrite.ml4
+++ b/ltac/g_rewrite.ml4
diff --git a/tactics/hightactics.mllib b/ltac/ltac.mllib
index 7987d774d1..7987d774d1 100644
--- a/tactics/hightactics.mllib
+++ b/ltac/ltac.mllib
diff --git a/tactics/rewrite.ml b/ltac/rewrite.ml
index fb04bee070..fb04bee070 100644
--- a/tactics/rewrite.ml
+++ b/ltac/rewrite.ml
diff --git a/tactics/rewrite.mli b/ltac/rewrite.mli
index 01709f29fb..01709f29fb 100644
--- a/tactics/rewrite.mli
+++ b/ltac/rewrite.mli
diff --git a/tactics/tacentries.ml b/ltac/tacentries.ml
index 711cd8d9d0..711cd8d9d0 100644
--- a/tactics/tacentries.ml
+++ b/ltac/tacentries.ml
diff --git a/tactics/tacentries.mli b/ltac/tacentries.mli
index 3cf0bc5cc9..3cf0bc5cc9 100644
--- a/tactics/tacentries.mli
+++ b/ltac/tacentries.mli
diff --git a/tactics/tacenv.ml b/ltac/tacenv.ml
index d2d3f3117f..d2d3f3117f 100644
--- a/tactics/tacenv.ml
+++ b/ltac/tacenv.ml
diff --git a/tactics/tacenv.mli b/ltac/tacenv.mli
index 88b54993b1..88b54993b1 100644
--- a/tactics/tacenv.mli
+++ b/ltac/tacenv.mli
diff --git a/tactics/tacintern.ml b/ltac/tacintern.ml
index a75805b4f8..a75805b4f8 100644
--- a/tactics/tacintern.ml
+++ b/ltac/tacintern.ml
diff --git a/tactics/tacintern.mli b/ltac/tacintern.mli
index 71ca354fa1..71ca354fa1 100644
--- a/tactics/tacintern.mli
+++ b/ltac/tacintern.mli
diff --git a/tactics/tacinterp.ml b/ltac/tacinterp.ml
index 4506f81596..4506f81596 100644
--- a/tactics/tacinterp.ml
+++ b/ltac/tacinterp.ml
diff --git a/tactics/tacinterp.mli b/ltac/tacinterp.mli
index 31327873e9..31327873e9 100644
--- a/tactics/tacinterp.mli
+++ b/ltac/tacinterp.mli
diff --git a/tactics/tacsubst.ml b/ltac/tacsubst.ml
index 4059877b75..4059877b75 100644
--- a/tactics/tacsubst.ml
+++ b/ltac/tacsubst.ml
diff --git a/tactics/tacsubst.mli b/ltac/tacsubst.mli
index c1bf272579..c1bf272579 100644
--- a/tactics/tacsubst.mli
+++ b/ltac/tacsubst.mli
diff --git a/tactics/tactic_debug.ml b/ltac/tactic_debug.ml
index d661f9677c..d661f9677c 100644
--- a/tactics/tactic_debug.ml
+++ b/ltac/tactic_debug.ml
diff --git a/tactics/tactic_debug.mli b/ltac/tactic_debug.mli
index 520fb41eff..520fb41eff 100644
--- a/tactics/tactic_debug.mli
+++ b/ltac/tactic_debug.mli
diff --git a/tactics/tactic_option.ml b/ltac/tactic_option.ml
index a5ba3b8371..a5ba3b8371 100644
--- a/tactics/tactic_option.ml
+++ b/ltac/tactic_option.ml
diff --git a/tactics/tactic_option.mli b/ltac/tactic_option.mli
index ed759a76db..ed759a76db 100644
--- a/tactics/tactic_option.mli
+++ b/ltac/tactic_option.mli
diff --git a/tactics/tauto.ml b/ltac/tauto.ml
index a86fdb98a9..a86fdb98a9 100644
--- a/tactics/tauto.ml
+++ b/ltac/tauto.ml
diff --git a/tactics/tauto.mli b/ltac/tauto.mli
index e69de29bb2..e69de29bb2 100644
--- a/tactics/tauto.mli
+++ b/ltac/tauto.mli
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 73ef7e1eda..ad1f8cbcc7 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 147759f5fc..f1ad2c2624 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";