aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/solvable/maximal.v
diff options
context:
space:
mode:
authorCyril Cohen2019-05-29 18:48:38 +0200
committerGitHub2019-05-29 18:48:38 +0200
commitbd4300d26ecbb43f7170e8da7eaaff1a13cc70b1 (patch)
treec685f3321960d062eedc51708c3f956d19a40515 /mathcomp/solvable/maximal.v
parent6bf8d7707ec6a1d9baf0ce8abaa31f1d681b3b99 (diff)
parentccceb6fbd3bd811b728f6e11dad3cf255a577801 (diff)
Replace eqVneq to destruct both x == y, but also y == x (#351)
Diffstat (limited to 'mathcomp/solvable/maximal.v')
-rw-r--r--mathcomp/solvable/maximal.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v
index f3d79fc..0dfb4d1 100644
--- a/mathcomp/solvable/maximal.v
+++ b/mathcomp/solvable/maximal.v
@@ -1642,4 +1642,4 @@ Qed.
End SCN.
-Arguments SCN_P {gT G A}. \ No newline at end of file
+Arguments SCN_P {gT G A}.