Merge pull request #145 from coq-community/add-try-test

add tests for try aac_rewrite and try aac_normalise
coq-community · Jun 27, 2024 · 5c133d3 · 5c133d3
2 parents 8ba7a8b + 8f5ebce
commit 5c133d3
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 0 deletions.
diff --git 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
@@ -5,3 +5,4 @@
 -R . Test
 
 aac_135.v
+aac_144.v
diff --git a/tests/aac_144.v 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.