Skip to content

Commit 251b7fa

Browse files
committed
add tests for try aac_rewrite and try aac_normalise
1 parent 2b36bb1 commit 251b7fa

File tree

3 files changed

+15
-0
lines changed

3 files changed

+15
-0
lines changed

CHANGELOG.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,10 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
55

66
## [Unreleased]
77

8+
### Added
9+
10+
- Tests for `try aac_rewrite` and `try aac_normalise` that failed on 8.19
11+
812
## [8.19.1] - 2024-06-01
913

1014
### Added

tests/_CoqProject

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,3 +5,4 @@
55
-R . Test
66

77
aac_135.v
8+
aac_144.v

tests/aac_144.v

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
From Coq Require Import ZArith.
2+
From AAC_tactics Require Import AAC.
3+
4+
Goal forall X:Prop, X->X.
5+
Succeed (try aac_rewrite Z.gcd_mod).
6+
Abort.
7+
8+
Goal forall X:Prop, X->X.
9+
Succeed (try aac_normalise).
10+
Abort.

0 commit comments

Comments
 (0)