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 2cf4d01695..df705034e7 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 8c1812da18..ea6b8b9194 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 46caca8d6f..23ad1fc017 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 e69de29bb2..e69de29bb2 100644
--- a/ltac/tauto.mli
+++ b/plugins/ltac/Ltac.v
diff --git a/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 28ff6df838..28ff6df838 100644
--- a/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
diff --git a/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index c5b26e6d56..c5b26e6d56 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 e67540c055..e67540c055 100644
--- a/ltac/evar_tactics.mli
+++ b/plugins/ltac/evar_tactics.mli
diff --git a/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 53b726432c..53b726432c 100644
--- a/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
diff --git a/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index b12187e18a..b12187e18a 100644
--- a/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
diff --git a/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 1223f6eb4b..1223f6eb4b 100644
--- a/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
diff --git a/ltac/extratactics.mli b/plugins/ltac/extratactics.mli
index 18334dafe7..18334dafe7 100644
--- a/ltac/extratactics.mli
+++ b/plugins/ltac/extratactics.mli
diff --git a/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index a37cf306e1..a37cf306e1 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 a28132a4b0..a28132a4b0 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 905653281c..905653281c 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 54229bb2ae..54229bb2ae 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 d286a58708..d286a58708 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 b1c4f58eb8..b1c4f58eb8 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 685c07c9a8..685c07c9a8 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 af1c7149da..af1c7149da 100644
--- a/ltac/ltac.mllib
+++ b/plugins/ltac/ltac_plugin.mllib
diff --git a/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 1d21118ae8..1d21118ae8 100644
--- a/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
diff --git a/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 810e1ec39a..810e1ec39a 100644
--- a/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
diff --git a/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index fccee6e40a..fccee6e40a 100644
--- a/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
diff --git a/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 86e3ea5484..86e3ea5484 100644
--- a/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
diff --git a/ltac/pptacticsig.mli b/plugins/ltac/pptacticsig.mli
index 74ddd377ad..74ddd377ad 100644
--- a/ltac/pptacticsig.mli
+++ b/plugins/ltac/pptacticsig.mli
diff --git a/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 2514ededb0..2514ededb0 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 e5e2e41975..e5e2e41975 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 8cb76d81c5..8cb76d81c5 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 3c5a109c0d..3c5a109c0d 100644
--- a/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
diff --git a/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 35c4483513..35c4483513 100644
--- a/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
diff --git a/ltac/tacarg.ml b/plugins/ltac/tacarg.ml
index 42552c4846..42552c4846 100644
--- a/ltac/tacarg.ml
+++ b/plugins/ltac/tacarg.ml
diff --git a/ltac/tacarg.mli b/plugins/ltac/tacarg.mli
index bfa423db20..bfa423db20 100644
--- a/ltac/tacarg.mli
+++ b/plugins/ltac/tacarg.mli
diff --git a/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index df38a42cb9..df38a42cb9 100644
--- a/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
diff --git a/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 0b67f8726e..0b67f8726e 100644
--- a/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
diff --git a/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 2e2b55be74..2e2b55be74 100644
--- a/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
diff --git a/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 969c118fb5..969c118fb5 100644
--- a/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
diff --git a/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index e3c2b4ad51..e3c2b4ad51 100644
--- a/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
diff --git a/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 94e14223aa..94e14223aa 100644
--- a/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
diff --git a/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 9c25a16457..9c25a16457 100644
--- a/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
diff --git a/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 763e0dc22e..763e0dc22e 100644
--- a/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
diff --git a/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 71ca354fa1..71ca354fa1 100644
--- a/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
diff --git a/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 32bcdfb6a4..32bcdfb6a4 100644
--- a/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
diff --git a/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 6f64981eff..6f64981eff 100644
--- a/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
diff --git a/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 55de583613..55de583613 100644
--- a/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
diff --git a/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli
index c1bf272579..c1bf272579 100644
--- a/ltac/tacsubst.mli
+++ b/plugins/ltac/tacsubst.mli
diff --git a/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 5cbddc7f64..5cbddc7f64 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 520fb41eff..520fb41eff 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 ef45ee47e1..ef45ee47e1 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 090207bcc3..090207bcc3 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 a5ba3b8371..a5ba3b8371 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 ed759a76db..ed759a76db 100644
--- a/ltac/tactic_option.mli
+++ b/plugins/ltac/tactic_option.mli
diff --git a/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 756958c2f0..756958c2f0 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 0000000000..e69de29bb2
--- /dev/null
+++ b/plugins/ltac/tauto.mli
diff --git a/plugins/ltac/vo.itarget b/plugins/ltac/vo.itarget
new file mode 100644
index 0000000000..a28fb770be
--- /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 48fbe0793c..edcd53005e 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 d9f8ed8815..cc1c44fe31 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