Skip to content
Snippets Groups Projects
Commit 224fa258 authored by Marco Maida's avatar Marco Maida
Browse files

Fixed error in classic

parent 66fe0910
No related branches found
No related tags found
1 merge request!104Support mathcomp 1.11.0 and Coq 8.12
Pipeline #32323 failed
......@@ -226,7 +226,7 @@ Module SuspensionTableConstruction.
by rewrite EQ /= in ALL; apply/eqP; rewrite eqb0.
}
move => /existsP [t0 /andP [/eqP EQ SUSP0]].
have MAX := @arg_maxP _ t0 (fun x=>(S j x == S j (ex j t)) && susp_at j x) id.
have MAX := @arg_maxnP _ t0 (fun x=>(S j x == S j (ex j t)) && susp_at j x) id.
feed MAX; simpl in MAX; first by rewrite EQ eq_refl SUSP0.
move: MAX => [m /andP [/eqP EQserv SUSPm] ALL]; clear EQ SUSP0 t0.
case (ltnP t m) => [LTm | GEm].
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment