diff options
Diffstat (limited to 'theories/Lists/SetoidPermutation.v')
| -rw-r--r-- | theories/Lists/SetoidPermutation.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v index 24b96514fd..f5ea303343 100644 --- a/theories/Lists/SetoidPermutation.v +++ b/theories/Lists/SetoidPermutation.v @@ -28,7 +28,7 @@ Inductive PermutationA : list A -> list A -> Prop := | permA_swap x y l : PermutationA (y :: x :: l) (x :: y :: l) | permA_trans l₁ l₂ l₃ : PermutationA l₁ l₂ -> PermutationA l₂ l₃ -> PermutationA l₁ l₃. -Local Hint Constructors PermutationA. +Local Hint Constructors PermutationA : core. Global Instance: Equivalence PermutationA. Proof. |