Skip to content

Commit

Permalink
make the linter happy
Browse files Browse the repository at this point in the history
  • Loading branch information
gares committed Jun 16, 2020
1 parent 8cbb01a commit 22ea81e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion test-suite/ssr/rewrtite_err_msg.v
Expand Up @@ -27,4 +27,4 @@ Lemma commute_abelian (gT : finGroupType) (G : group gT)
mul g g' = mul g' g.
Proof.
Fail rewrite (centsP _). (* fails but without an anomaly *)
Abort.
Abort.

0 comments on commit 22ea81e

Please sign in to comment.