From 66c523bcac8b64e202baa084bf24f5b57c61fcd6 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 6 Mar 2018 16:12:28 +0000 Subject: [stdlib] Do not use “Require” inside sections MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- plugins/rtauto/Rtauto.v | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'plugins/rtauto') 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 : -- cgit v1.2.3