Skip to content

Commit 6b46a2a

Browse files
committed
Update to MC-dev
1 parent 48f4bf7 commit 6b46a2a

1 file changed

Lines changed: 2 additions & 0 deletions

File tree

theories/SymGroup/Bruhat.v

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,8 @@ From mathcomp Require Import ssralg matrix.
5353
Require Import permcomp tools permuted combclass congr presentSn.
5454
Require Import std ordtype.
5555

56+
Set SsrOldRewriteGoalsOrder. (* change to Unset and remove the line when requiring MathComp >= 2.6 *)
57+
5658
Set Implicit Arguments.
5759
Unset Strict Implicit.
5860
Unset Printing Implicit Defensive.

0 commit comments

Comments
 (0)