diff options
| -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. |