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 /theories/Sorting | |
| parent | 144517d764f11b8b79e8f7adfeca0d075dd4ac19 (diff) | |
[stdlib] Do not use “Require” inside sections
Diffstat (limited to 'theories/Sorting')
| -rw-r--r-- | theories/Sorting/Heap.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |