Ltac as a plugin.

This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.

55 files changed, 14 insertions, 11 deletions

diff --git a/Makefile.common b/Makefile.common
index 2cf4d0169..df705034e 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -55,14 +55,14 @@ MKDIR:=install -d
 CORESRCDIRS:=\
   config 	lib		kernel	intf	kernel/byterun	library \
   engine 	pretyping	interp	proofs	parsing 	printing \
-  tactics 	vernac		stm		toplevel 	ltac
+  tactics 	vernac		stm		toplevel
 
 PLUGINDIRS:=\
   omega		romega 		micromega 	quote \
   setoid_ring 	extraction 	fourier \
   cc 		funind 		firstorder 	derive \
   rtauto 	nsatz           syntax          decl_mode	btauto \
-  ssrmatching
+  ssrmatching	ltac
 
 SRCDIRS:=\
   $(CORESRCDIRS)  \
@@ -77,14 +77,13 @@ 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 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 vernac/vernac.cma \
-	stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma ltac/ltac.cma
+	stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma
 
 TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
 
@@ -120,6 +119,7 @@ OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \
         string_syntax_plugin.cmo )
 DECLMODECMO:=plugins/decl_mode/decl_mode_plugin.cmo
 DERIVECMO:=plugins/derive/derive_plugin.cmo
+LTACCMO:=plugins/ltac/ltac_plugin.cmo
 SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
 
 PLUGINSCMO:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) $(DECLMODECMO) \
@@ -127,7 +127,7 @@ PLUGINSCMO:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) $(DECLMODECMO) \
         $(FOURIERCMO) $(EXTRACTIONCMO) \
         $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
         $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \
-	$(DERIVECMO) $(SSRMATCHINGCMO)
+	$(DERIVECMO) $(SSRMATCHINGCMO) $(LTACCMO)
 
 ifeq ($(HASNATDYNLINK)-$(BEST),false-opt)
  STATICPLUGINS:=$(PLUGINSCMO)
diff --git a/Makefile.dev b/Makefile.dev
index 8c1812da1..ea6b8b919 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -121,10 +121,9 @@ pretyping: pretyping/pretyping.cma
 highparsing: parsing/highparsing.cma
 stm: stm/stm.cma
 toplevel: toplevel/toplevel.cma
-ltac: ltac/ltac.cma
 
 .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping
-.PHONY: engine highparsing stm toplevel ltac
+.PHONY: engine highparsing stm toplevel
 
 ######################
 ### 3) theories files
@@ -183,6 +182,7 @@ RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO))
 EXTRACTIONVO:=$(filter plugins/extraction/%, $(PLUGINSVO))
 CCVO:=
 DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO))
+LTACVO:=$(filter plugins/ltac/%, $(PLUGINSVO))
 
 omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO)
 micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
@@ -194,9 +194,10 @@ funind: $(FUNINDCMO) $(FUNINDVO)
 cc: $(CCVO) $(CCCMO)
 rtauto: $(RTAUTOVO) $(RTAUTOCMO)
 btauto: $(BTAUTOVO) $(BTAUTOCMO)
+ltac: $(LTACVO) $(LTACCMO)
 
 .PHONY: omega micromega setoid_ring nsatz extraction
-.PHONY: fourier funind cc rtauto btauto
+.PHONY: fourier funind cc rtauto btauto ltac
 
 #################################
 ### Misc other development rules
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 46caca8d6..23ad1fc01 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -32,6 +32,6 @@ exec $OCAMLDEBUG \
         -I $COQTOP/plugins/ring       -I $COQTOP/plugins/romega \
 	-I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
         -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
-        -I $COQTOP/plugins/xml \
+        -I $COQTOP/plugins/xml        -I $COQTOP/plugins/ltac \
         -I $COQTOP/ide \
 	"$@"
diff --git a/ltac/tauto.mli b/plugins/ltac/Ltac.v
index e69de29bb..e69de29bb 100644
--- a/ltac/tauto.mli
+++ b/plugins/ltac/Ltac.v
diff --git a/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 28ff6df83..28ff6df83 100644
--- a/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
diff --git a/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index c5b26e6d5..c5b26e6d5 100644
--- a/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
diff --git a/ltac/evar_tactics.mli b/plugins/ltac/evar_tactics.mli
index e67540c05..e67540c05 100644
--- a/ltac/evar_tactics.mli
+++ b/plugins/ltac/evar_tactics.mli
diff --git a/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 53b726432..53b726432 100644
--- a/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
diff --git a/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index b12187e18..b12187e18 100644
--- a/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
diff --git a/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 1223f6eb4..1223f6eb4 100644
--- a/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
diff --git a/ltac/extratactics.mli b/plugins/ltac/extratactics.mli
index 18334dafe..18334dafe 100644
--- a/ltac/extratactics.mli
+++ b/plugins/ltac/extratactics.mli
diff --git a/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index a37cf306e..a37cf306e 100644
--- a/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
diff --git a/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index a28132a4b..a28132a4b 100644
--- a/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
diff --git a/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4
index 905653281..905653281 100644
--- a/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
diff --git a/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 54229bb2a..54229bb2a 100644
--- a/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
diff --git a/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index d286a5870..d286a5870 100644
--- a/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
diff --git a/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index b1c4f58eb..b1c4f58eb 100644
--- a/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
diff --git a/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 685c07c9a..685c07c9a 100644
--- a/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
diff --git a/ltac/ltac.mllib b/plugins/ltac/ltac_plugin.mllib
index af1c7149d..af1c7149d 100644
--- a/ltac/ltac.mllib
+++ b/plugins/ltac/ltac_plugin.mllib
diff --git a/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 1d21118ae..1d21118ae 100644
--- a/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
diff --git a/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 810e1ec39..810e1ec39 100644
--- a/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
diff --git a/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index fccee6e40..fccee6e40 100644
--- a/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
diff --git a/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 86e3ea548..86e3ea548 100644
--- a/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
diff --git a/ltac/pptacticsig.mli b/plugins/ltac/pptacticsig.mli
index 74ddd377a..74ddd377a 100644
--- a/ltac/pptacticsig.mli
+++ b/plugins/ltac/pptacticsig.mli
diff --git a/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 2514ededb..2514ededb 100644
--- a/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
diff --git a/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli
index e5e2e4197..e5e2e4197 100644
--- a/ltac/profile_ltac.mli
+++ b/plugins/ltac/profile_ltac.mli
diff --git a/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4
index 8cb76d81c..8cb76d81c 100644
--- a/ltac/profile_ltac_tactics.ml4
+++ b/plugins/ltac/profile_ltac_tactics.ml4
diff --git a/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3c5a109c0..3c5a109c0 100644
--- a/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
diff --git a/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 35c448351..35c448351 100644
--- a/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
diff --git a/ltac/tacarg.ml b/plugins/ltac/tacarg.ml
index 42552c484..42552c484 100644
--- a/ltac/tacarg.ml
+++ b/plugins/ltac/tacarg.ml
diff --git a/ltac/tacarg.mli b/plugins/ltac/tacarg.mli
index bfa423db2..bfa423db2 100644
--- a/ltac/tacarg.mli
+++ b/plugins/ltac/tacarg.mli
diff --git a/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index df38a42cb..df38a42cb 100644
--- a/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
diff --git a/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 0b67f8726..0b67f8726 100644
--- a/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
diff --git a/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 2e2b55be7..2e2b55be7 100644
--- a/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
diff --git a/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 969c118fb..969c118fb 100644
--- a/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
diff --git a/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index e3c2b4ad5..e3c2b4ad5 100644
--- a/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
diff --git a/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 94e14223a..94e14223a 100644
--- a/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
diff --git a/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 9c25a1645..9c25a1645 100644
--- a/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
diff --git a/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 763e0dc22..763e0dc22 100644
--- a/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
diff --git a/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 71ca354fa..71ca354fa 100644
--- a/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
diff --git a/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 32bcdfb6a..32bcdfb6a 100644
--- a/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
diff --git a/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 6f64981ef..6f64981ef 100644
--- a/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
diff --git a/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 55de58361..55de58361 100644
--- a/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
diff --git a/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli
index c1bf27257..c1bf27257 100644
--- a/ltac/tacsubst.mli
+++ b/plugins/ltac/tacsubst.mli
diff --git a/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 5cbddc7f6..5cbddc7f6 100644
--- a/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
diff --git a/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 520fb41ef..520fb41ef 100644
--- a/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
diff --git a/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index ef45ee47e..ef45ee47e 100644
--- a/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
diff --git a/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli
index 090207bcc..090207bcc 100644
--- a/ltac/tactic_matching.mli
+++ b/plugins/ltac/tactic_matching.mli
diff --git a/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml
index a5ba3b837..a5ba3b837 100644
--- a/ltac/tactic_option.ml
+++ b/plugins/ltac/tactic_option.ml
diff --git a/ltac/tactic_option.mli b/plugins/ltac/tactic_option.mli
index ed759a76d..ed759a76d 100644
--- a/ltac/tactic_option.mli
+++ b/plugins/ltac/tactic_option.mli
diff --git a/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 756958c2f..756958c2f 100644
--- a/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
diff --git a/plugins/ltac/tauto.mli b/plugins/ltac/tauto.mli
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/plugins/ltac/tauto.mli
diff --git a/plugins/ltac/vo.itarget b/plugins/ltac/vo.itarget
new file mode 100644
index 000000000..a28fb770b
--- /dev/null
+++ b/plugins/ltac/vo.itarget
@@ -0,0 +1 @@
+Ltac.vo
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 48fbe0793..edcd53005 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -88,9 +88,12 @@ Open Scope type_scope.
 
 (** ML Tactic Notations *)
 
+Declare ML Module "ltac_plugin".
 Declare ML Module "coretactics".
 Declare ML Module "extratactics".
 Declare ML Module "g_auto".
 Declare ML Module "g_class".
 Declare ML Module "g_eqdecide".
 Declare ML Module "g_rewrite".
+
+Global Set Default Proof Mode "Classic".
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d9f8ed881..cc1c44fe3 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -603,8 +603,6 @@ let init_toplevel arglist =
   init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
   Lib.init();
-  (* Default Proofb Mode starts with an alternative default. *)
-  Goptions.set_string_option_value ["Default";"Proof";"Mode"] "Classic";
   begin
     try
       let extras = parse_args arglist in