diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-02-16 00:30:20 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-12 14:04:11 +0200 |
| commit | 4a0e4ee76663a12e3cb3d22ce77b0d37a5830af5 (patch) | |
| tree | c3b045f597cfd3f8499e476960ff3e0a19516243 /plugins/btauto | |
| 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 'plugins/btauto')
| -rw-r--r-- | plugins/btauto/Algebra.v | 2 | ||||
| -rw-r--r-- | plugins/btauto/Reflect.v | 2 | ||||
| -rw-r--r-- | plugins/btauto/g_btauto.ml4 | 2 |
3 files changed, 4 insertions, 2 deletions
diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v index 795211c20..bc5a39002 100644 --- a/plugins/btauto/Algebra.v +++ b/plugins/btauto/Algebra.v @@ -1,4 +1,4 @@ -Require Import Bool PArith DecidableClass ROmega. +Require Import Bool PArith DecidableClass Omega ROmega. Ltac bool := repeat match goal with diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v index e31948ffe..8a95d5b4b 100644 --- a/plugins/btauto/Reflect.v +++ b/plugins/btauto/Reflect.v @@ -1,4 +1,4 @@ -Require Import Bool DecidableClass Algebra Ring PArith ROmega. +Require Import Bool DecidableClass Algebra Ring PArith ROmega Omega. Section Bool. diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4 index a45203d3d..ce99756e0 100644 --- a/plugins/btauto/g_btauto.ml4 +++ b/plugins/btauto/g_btauto.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "btauto_plugin" + TACTIC EXTEND btauto | [ "btauto" ] -> [ Refl_btauto.Btauto.tac ] END |