diff options
Diffstat (limited to 'plugins/rtauto')
| -rw-r--r-- | plugins/rtauto/Bintree.v | 2 | ||||
| -rw-r--r-- | plugins/rtauto/Rtauto.v | 1 |
2 files changed, 0 insertions, 3 deletions
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 769869584d..6c250ef4f9 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -9,8 +9,6 @@ Require Export List. Require Export BinPos. -Unset Boxed Definitions. - Open Scope positive_scope. Ltac clean := try (simpl; congruence). diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index e805428313..f5d452f7e6 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -10,7 +10,6 @@ Require Export List. Require Export Bintree. Require Import Bool. -Unset Boxed Definitions. Declare ML Module "rtauto_plugin". |