diff --git a/CHANGELOG.md b/CHANGELOG.md index 715bb93..81f22bc 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,10 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ## [Unreleased] +### Added + +- Tests for `try aac_rewrite` and `try aac_normalise` that failed on 8.19 + ## [8.19.1] - 2024-06-01 ### Added diff --git a/tests/_CoqProject b/tests/_CoqProject index 6f9a599..cec9696 100644 --- a/tests/_CoqProject +++ b/tests/_CoqProject @@ -5,3 +5,4 @@ -R . Test aac_135.v +aac_144.v diff --git a/tests/aac_144.v b/tests/aac_144.v new file mode 100644 index 0000000..37d77f1 --- /dev/null +++ b/tests/aac_144.v @@ -0,0 +1,10 @@ +From Coq Require Import ZArith. +From AAC_tactics Require Import AAC. + +Goal forall X:Prop, X->X. +Succeed (try aac_rewrite Z.gcd_mod). +Abort. + +Goal forall X:Prop, X->X. +Succeed (try aac_normalise). +Abort.