From 251b7fa03535e6e1668311998e45c99ef5f19d43 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Thu, 27 Jun 2024 20:51:51 +0200
Subject: [PATCH] add tests for try aac_rewrite and try aac_normalise

---
 CHANGELOG.md      |  4 ++++
 tests/_CoqProject |  1 +
 tests/aac_144.v   | 10 ++++++++++
 3 files changed, 15 insertions(+)
 create mode 100644 tests/aac_144.v

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.