aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--Makefile.common10
-rw-r--r--Makefile.dev7
-rw-r--r--dev/ocamldebug-coq.run2
-rw-r--r--plugins/ltac/Ltac.v (renamed from ltac/tauto.mli)0
-rw-r--r--plugins/ltac/coretactics.ml4 (renamed from ltac/coretactics.ml4)0
-rw-r--r--plugins/ltac/evar_tactics.ml (renamed from ltac/evar_tactics.ml)0
-rw-r--r--plugins/ltac/evar_tactics.mli (renamed from ltac/evar_tactics.mli)0
-rw-r--r--plugins/ltac/extraargs.ml4 (renamed from ltac/extraargs.ml4)0
-rw-r--r--plugins/ltac/extraargs.mli (renamed from ltac/extraargs.mli)0
-rw-r--r--plugins/ltac/extratactics.ml4 (renamed from ltac/extratactics.ml4)0
-rw-r--r--plugins/ltac/extratactics.mli (renamed from ltac/extratactics.mli)0
-rw-r--r--plugins/ltac/g_auto.ml4 (renamed from ltac/g_auto.ml4)0
-rw-r--r--plugins/ltac/g_class.ml4 (renamed from ltac/g_class.ml4)0
-rw-r--r--plugins/ltac/g_eqdecide.ml4 (renamed from ltac/g_eqdecide.ml4)0
-rw-r--r--plugins/ltac/g_ltac.ml4 (renamed from ltac/g_ltac.ml4)0
-rw-r--r--plugins/ltac/g_obligations.ml4 (renamed from ltac/g_obligations.ml4)0
-rw-r--r--plugins/ltac/g_rewrite.ml4 (renamed from ltac/g_rewrite.ml4)0
-rw-r--r--plugins/ltac/g_tactic.ml4 (renamed from ltac/g_tactic.ml4)0
-rw-r--r--plugins/ltac/ltac_plugin.mllib (renamed from ltac/ltac.mllib)0
-rw-r--r--plugins/ltac/pltac.ml (renamed from ltac/pltac.ml)0
-rw-r--r--plugins/ltac/pltac.mli (renamed from ltac/pltac.mli)0
-rw-r--r--plugins/ltac/pptactic.ml (renamed from ltac/pptactic.ml)0
-rw-r--r--plugins/ltac/pptactic.mli (renamed from ltac/pptactic.mli)0
-rw-r--r--plugins/ltac/pptacticsig.mli (renamed from ltac/pptacticsig.mli)0
-rw-r--r--plugins/ltac/profile_ltac.ml (renamed from ltac/profile_ltac.ml)0
-rw-r--r--plugins/ltac/profile_ltac.mli (renamed from ltac/profile_ltac.mli)0
-rw-r--r--plugins/ltac/profile_ltac_tactics.ml4 (renamed from ltac/profile_ltac_tactics.ml4)0
-rw-r--r--plugins/ltac/rewrite.ml (renamed from ltac/rewrite.ml)0
-rw-r--r--plugins/ltac/rewrite.mli (renamed from ltac/rewrite.mli)0
-rw-r--r--plugins/ltac/tacarg.ml (renamed from ltac/tacarg.ml)0
-rw-r--r--plugins/ltac/tacarg.mli (renamed from ltac/tacarg.mli)0
-rw-r--r--plugins/ltac/taccoerce.ml (renamed from ltac/taccoerce.ml)0
-rw-r--r--plugins/ltac/taccoerce.mli (renamed from ltac/taccoerce.mli)0
-rw-r--r--plugins/ltac/tacentries.ml (renamed from ltac/tacentries.ml)0
-rw-r--r--plugins/ltac/tacentries.mli (renamed from ltac/tacentries.mli)0
-rw-r--r--plugins/ltac/tacenv.ml (renamed from ltac/tacenv.ml)0
-rw-r--r--plugins/ltac/tacenv.mli (renamed from ltac/tacenv.mli)0
-rw-r--r--plugins/ltac/tacexpr.mli (renamed from ltac/tacexpr.mli)0
-rw-r--r--plugins/ltac/tacintern.ml (renamed from ltac/tacintern.ml)0
-rw-r--r--plugins/ltac/tacintern.mli (renamed from ltac/tacintern.mli)0
-rw-r--r--plugins/ltac/tacinterp.ml (renamed from ltac/tacinterp.ml)0
-rw-r--r--plugins/ltac/tacinterp.mli (renamed from ltac/tacinterp.mli)0
-rw-r--r--plugins/ltac/tacsubst.ml (renamed from ltac/tacsubst.ml)0
-rw-r--r--plugins/ltac/tacsubst.mli (renamed from ltac/tacsubst.mli)0
-rw-r--r--plugins/ltac/tactic_debug.ml (renamed from ltac/tactic_debug.ml)0
-rw-r--r--plugins/ltac/tactic_debug.mli (renamed from ltac/tactic_debug.mli)0
-rw-r--r--plugins/ltac/tactic_matching.ml (renamed from ltac/tactic_matching.ml)0
-rw-r--r--plugins/ltac/tactic_matching.mli (renamed from ltac/tactic_matching.mli)0
-rw-r--r--plugins/ltac/tactic_option.ml (renamed from ltac/tactic_option.ml)0
-rw-r--r--plugins/ltac/tactic_option.mli (renamed from ltac/tactic_option.mli)0
-rw-r--r--plugins/ltac/tauto.ml (renamed from ltac/tauto.ml)0
-rw-r--r--plugins/ltac/tauto.mli0
-rw-r--r--plugins/ltac/vo.itarget1
-rw-r--r--theories/Init/Notations.v3
-rw-r--r--toplevel/coqtop.ml2
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