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 --- theories/Sorting/Heap.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Sorting') diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 8f583be97..d9e5ad676 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -136,7 +136,7 @@ Section defs. (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) -> (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) -> merge_lem l1 l2. - Require Import Morphisms. + Import Morphisms. Instance: Equivalence (@meq A). Proof. constructor; auto with datatypes. red. apply meq_trans. Defined. -- cgit v1.2.3