diff options
author | 2014-02-16 00:30:20 +0100 | |
---|---|---|
committer | 2014-05-12 14:04:11 +0200 | |
commit | 4a0e4ee76663a12e3cb3d22ce77b0d37a5830af5 (patch) | |
tree | c3b045f597cfd3f8499e476960ff3e0a19516243 /theories/Init/Notations.v | |
parent | d72e57a9e657c9d2563f2b49574464325135b518 (diff) |
Now parsing rules of ML-declared tactics are only made available after the
corresponding Declare ML Module command. This changes essentially two
things:
1. ML plugins are forced to use the DECLARE PLUGIN statement before any
TACTIC EXTEND statement. The plugin name must be exactly the string passed to
the Declare ML Module command.
2. ML tactics are only made available after the Coq module that does the
corresponding Declare ML Module is imported. This may break a few things,
as it already broke quite some uses of omega in the stdlib.
Diffstat (limited to 'theories/Init/Notations.v')
-rw-r--r-- | theories/Init/Notations.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index d3b65c174..7cf478e18 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -80,3 +80,12 @@ Delimit Scope core_scope with core. Open Scope core_scope. Open Scope type_scope. + +(** ML Tactic Notations *) + +Declare ML Module "extratactics". +Declare ML Module "eauto". +Declare ML Module "g_class". +Declare ML Module "g_eqdecide". +Declare ML Module "g_rewrite". +Declare ML Module "tauto". |