diff options
| -rw-r--r-- | Makefile.common | 10 | ||||
| -rw-r--r-- | Makefile.dev | 7 | ||||
| -rw-r--r-- | dev/ocamldebug-coq.run | 2 | ||||
| -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.mli | 0 | ||||
| -rw-r--r-- | plugins/ltac/vo.itarget | 1 | ||||
| -rw-r--r-- | theories/Init/Notations.v | 3 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 |
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 |