Merge PR#309: Ltac as a plugin

86 files changed, 76 insertions, 22 deletions

diff --git a/.gitignore b/.gitignore
index 7434f6212..35cdf9b4e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -122,10 +122,10 @@ g_*.ml
 ide/project_file.ml
 parsing/compat.ml
 parsing/cLexer.ml
-ltac/coretactics.ml
-ltac/extratactics.ml
-ltac/extraargs.ml
-ltac/profile_ltac_tactics.ml
+plugins/ltac/coretactics.ml
+plugins/ltac/extratactics.ml
+plugins/ltac/extraargs.ml
+plugins/ltac/profile_ltac_tactics.ml
 ide/coqide_main.ml
 plugins/ssrmatching/ssrmatching.ml
 
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/doc/changes.txt b/dev/doc/changes.txt
index f54f3fcc8..8d2d05590 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -40,6 +40,24 @@ important things:
 - Some printing functions were moved from Pptactic to Pputils
 - A part of Tacexpr has been moved to Tactypes
 
+The folder itself has been turned into a plugin. This does not change much,
+but because it is a packed plugin, it may wreak havoc for third-party plugins
+depending on any module defined in the ltac/ directory. Namely, even if
+everything looks OK at compile time, a plugin can fail to load at link time
+because it mistakenly looks for a module Foo instead of Ltac_plugin.Foo, with
+an error of the form:
+
+Error: while loading myplugin.cmxs, no implementation available for Foo.
+
+In particular, most EXTEND macros will trigger this problem even if they
+seemingly do not use any Ltac module, as their expansion do.
+
+The solution is simple, and consists in adding a statement "open Ltac_plugin"
+in each file using a Ltac module, before such a module is actually called. An
+alternative solution would be to fully qualify Ltac modules, e.g. turning any
+call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not
+work for EXTEND macros though.
+
 ** Error handling **
 
 - All error functions now take an optional parameter `?loc:Loc.t`. For
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 26cfcc8ae..3850c05fd 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/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4
index f3e2c99f4..298027448 100644
--- a/plugins/btauto/g_btauto.ml4
+++ b/plugins/btauto/g_btauto.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+open Ltac_plugin
+
 DECLARE PLUGIN "btauto_plugin"
 
 TACTIC EXTEND btauto
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 6f6811334..7e76854b1 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Cctac
 open Stdarg
 
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index f68c01b18..2b63ed6d6 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open CErrors
 open Util
 open Names
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index e19dc86c4..deb2ede1d 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open CErrors
 open Util
 open Pp
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 18a35c6cf..a71d20f0d 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -10,6 +10,7 @@
 
 DECLARE PLUGIN "decl_mode_plugin"
 
+open Ltac_plugin
 open Compat
 open Pp
 open Decl_expr
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index 59a0bb5a2..f5de638ed 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open CErrors
 open Pp
 open Decl_expr
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index e1d6bb4a8..3ed959cf2 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -12,6 +12,7 @@ DECLARE PLUGIN "extraction_plugin"
 
 (* ML names *)
 
+open Ltac_plugin
 open Genarg
 open Stdarg
 open Pcoq.Prim
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 260e86ad6..e28d6aa62 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+open Ltac_plugin
 open Formula
 open Sequent
 open Ground
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 628af4e71..d6cd7e2a0 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open Formula
 open Sequent
 open Rules
diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4
index 7c665ae7b..1960fa835 100644
--- a/plugins/fourier/g_fourier.ml4
+++ b/plugins/fourier/g_fourier.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open FourierR
 
 DECLARE PLUGIN "fourier_plugin"
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 6603a95a8..368b23be3 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 (*i camlp4deps: "grammar/grammar.cma" i*)
+open Ltac_plugin
 open Compat
 open Util
 open Term
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index c8b4e4833..70333b063 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open Tacexpr
 open Declarations
 open CErrors
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.mlpack
index af1c7149d..af1c7149d 100644
--- a/ltac/ltac.mllib
+++ b/plugins/ltac/ltac_plugin.mlpack
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/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 79020ed03..ccb6daa11 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -16,6 +16,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Stdarg
 open Tacarg
 
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index 5f906a8da..195dec362 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -1,5 +1,3 @@
-DECLARE PLUGIN "nsatz_plugin"
-
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
@@ -10,6 +8,8 @@ DECLARE PLUGIN "nsatz_plugin"
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
+
 DECLARE PLUGIN "nsatz_plugin"
 
 TACTIC EXTEND nsatz_compute
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 27115abec..6b711a176 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -17,6 +17,7 @@
 
 DECLARE PLUGIN "omega_plugin"
 
+open Ltac_plugin
 open Names
 open Coq_omega
 open Stdarg
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index e7e6ecef9..f2c021f59 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Names
 open Misctypes
 open Tacexpr
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 2f38688d1..9a54ad778 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -10,6 +10,7 @@
 
 DECLARE PLUGIN "romega_plugin"
 
+open Ltac_plugin
 open Names
 open Refl_omega
 open Stdarg
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index d27b04834..7e58ef9a3 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+open Ltac_plugin
+
 DECLARE PLUGIN "rtauto_plugin"
 
 TACTIC EXTEND rtauto
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 367a13333..35d6768c1 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -8,6 +8,7 @@
 
 module Search = Explore.Make(Proof_search)
 
+open Ltac_plugin
 open CErrors
 open Util
 open Term
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 0987c44ae..707ff79a6 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Pp
 open Util
 open Libnames
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 657efe175..59f23a637 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open Pp
 open CErrors
 open Util
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index fc988a2c5..f4f6efa4a 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -15,6 +15,7 @@ let frozen_lexer = CLexer.freeze () ;;
 (*i camlp4use: "pa_extend.cmo" i*)
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Names
 open Pp
 open Pcoq
diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
index a54768507..4b4f81dbc 100644
--- a/test-suite/bugs/closed/3612.v
+++ b/test-suite/bugs/closed/3612.v
@@ -38,8 +38,11 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P)
            (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2),
 p = q.
 
+Declare ML Module "ltac_plugin".
 Declare ML Module "coretactics".
 
+Set Default Proof Mode "Classic".
+
 Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x))
             (xx : @paths (@sigT A (fun x0 : A => B x0)) x x),
        @paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index fc4c171e2..8687eaab0 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -2,7 +2,9 @@
 (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *)
 (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
+Declare ML Module "ltac_plugin".
 Declare ML Module "coretactics".
+Set Default Proof Mode "Classic".
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Reserved Notation "x = y" (at level 70, no associativity).
 Delimit Scope type_scope with type.
diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v
index d34a2b8b1..816bc845f 100644
--- a/test-suite/bugs/closed/4121.v
+++ b/test-suite/bugs/closed/4121.v
@@ -4,6 +4,8 @@ Unset Strict Universe Declaration.
 (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0
    coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897af8186cb1bdfb04fd4f88eca677) *)
 
+Declare ML Module "ltac_plugin".
+
 Set Universe Polymorphism.
 Class Contr_internal (A : Type) := BuildContr { center : A }.
 Arguments center A {_}.
@@ -13,4 +15,4 @@ Definition contr_paths_contr0 {A} `{Contr A} : Contr A := {| center := center A
 Instance contr_paths_contr1 {A} `{Contr A} : Contr A := {| center := center A |}.
 Check @contr_paths_contr0@{i}.
 Check @contr_paths_contr1@{i}. (* Error: Universe instance should have length 2 *)
-(** It should have length 1, just like contr_paths_contr0 *)
\ No newline at end of file
+(** It should have length 1, just like contr_paths_contr0 *)
diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v
index 08628377f..c6fcc24b6 100644
--- a/test-suite/bugs/closed/4527.v
+++ b/test-suite/bugs/closed/4527.v
@@ -5,6 +5,7 @@ then from 269 lines to 255 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 
 4.01.0
    coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v
index ae17fb145..64c7fd8eb 100644
--- a/test-suite/bugs/closed/4533.v
+++ b/test-suite/bugs/closed/4533.v
@@ -5,6 +5,7 @@ then from 285 lines to 271 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 
 4.01.0
    coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
@@ -223,4 +224,4 @@ v = _) r,
     | [ |- p2 @ p0 @ p1 @ eissect (to O A) (g x) = r ] => idtac "good"
     | [ |- ?G ] => fail 1 "bad" G
     end.
-    Fail rewrite concat_p_pp.
\ No newline at end of file
+    Fail rewrite concat_p_pp.
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index da140c931..64dd8c304 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -2,6 +2,7 @@
 (* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0
    coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
@@ -1004,4 +1005,4 @@ Proof.
   Fail Timeout 1 Time rewrite !loops_functor_group.
   (* 0.004 s in 8.5rc1, 8.677 s in 8.5 *)
   Timeout 1 do 3 rewrite loops_functor_group.
-Abort.
\ No newline at end of file
+Abort.
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/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 624b9ced7..4842a8915 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -50,9 +50,9 @@ let section s =
 let lib_dirs =
   ["kernel"; "lib"; "library"; "parsing";
    "pretyping"; "interp"; "printing"; "intf";
-   "proofs"; "tactics"; "tools"; "ltacprof";
+   "proofs"; "tactics"; "tools";
    "vernac"; "stm"; "toplevel"; "grammar"; "config";
-   "ltac"; "engine"]
+   "engine"]
 
 
 let usage () =
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