diff options
| author | Enrico Tassi | 2020-06-16 14:09:50 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2020-06-16 14:09:50 +0200 |
| commit | 22ea81efe0111381be372d88821da8b2fa76be71 (patch) | |
| tree | e5a6b4379d248c91f384f9082d22d9517fb1c3a9 | |
| parent | 8cbb01a852c950f044c6f2c9a9ada2626d2bbfc5 (diff) | |
make the linter happy
| -rw-r--r-- | test-suite/ssr/rewrtite_err_msg.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/ssr/rewrtite_err_msg.v b/test-suite/ssr/rewrtite_err_msg.v index d749fd264b..2bbbff433c 100644 --- a/test-suite/ssr/rewrtite_err_msg.v +++ b/test-suite/ssr/rewrtite_err_msg.v @@ -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.
\ No newline at end of file +Abort. |