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/Sets/Uniset.v | |
parent | 144517d764f11b8b79e8f7adfeca0d075dd4ac19 (diff) |
[stdlib] Do not use “Require” inside sections
Diffstat (limited to 'theories/Sets/Uniset.v')
-rw-r--r-- | theories/Sets/Uniset.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 95ba93232..7940bda1a 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -13,7 +13,7 @@ (* G. Huet 1-9-95 *) (* Updated Papageno 12/98 *) -Require Import Bool. +Require Import Bool Permut. Set Implicit Arguments. @@ -140,8 +140,6 @@ Hint Resolve seq_right. (** Here we should make uniset an abstract datatype, by hiding [Charac], [union], [charac]; all further properties are proved abstractly *) -Require Import Permut. - Lemma union_rotate : forall x y z:uniset, seq (union x (union y z)) (union z (union x y)). Proof. |