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/Logic | |
| parent | 144517d764f11b8b79e8f7adfeca0d075dd4ac19 (diff) | |
[stdlib] Do not use “Require” inside sections
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/ChoiceFacts.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 9fd52866e..238ac7df0 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -28,6 +28,8 @@ intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005. [[Werner97]] Benjamin Werner, Sets in Types, Types in Sets, TACS, 1997. *) +Require Import RelationClasses Logic. + Set Implicit Arguments. Local Unset Intuition Negation Unfolding. @@ -125,8 +127,6 @@ Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) := formulation of choice); Note also a typo in its intended formulation in [[Werner97]]. *) -Require Import RelationClasses Logic. - Definition RepresentativeFunctionalChoice_on := forall R:A->A->Prop, (Equivalence R) -> |