diff options
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 |