diff options
Diffstat (limited to 'theories/Relations')
| -rw-r--r-- | theories/Relations/Relation_Operators.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index 8fea0abc4..39e0331d5 100644 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -17,7 +17,6 @@ (************************************************************************) Require Import Relation_Definitions. -Require Import List. (** * Some operators to build relations *) @@ -187,6 +186,7 @@ Section Swap. | sp_swap x y (p:A * A) : symprod A A R R (x, y) p -> swapprod (y, x) p. End Swap. +Local Open Scope list_scope. Section Lexicographic_Exponentiation. |