diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-03-06 16:12:28 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-03-07 17:31:46 +0000 |
| commit | 66c523bcac8b64e202baa084bf24f5b57c61fcd6 (patch) | |
| tree | b3772186b0829ff27c76c05ae1bec44173758c01 /plugins/rtauto | |
| parent | 144517d764f11b8b79e8f7adfeca0d075dd4ac19 (diff) | |
[stdlib] Do not use “Require” inside sections
Diffstat (limited to 'plugins/rtauto')
| -rw-r--r-- | plugins/rtauto/Rtauto.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index db17c0d65..19b3ab397 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -11,7 +11,7 @@ Require Export List. Require Export Bintree. -Require Import Bool. +Require Import Bool BinPos. Declare ML Module "rtauto_plugin". @@ -98,8 +98,6 @@ match F with | F_push H hyps0 F0 => interp_ctx hyps0 F0 ([[H]] -> G) end. -Require Export BinPos. - Ltac wipe := intros;simpl;constructor. Lemma compose0 : |