Skip to content

Commit d5f7c81

Browse files
authored
Merge pull request #90 from SkySkimmer/univ-name-fix
Use forward compatible univ names in test for #16803
2 parents f05e12d + b57c250 commit d5f7c81

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

test-suite/bugs/bug_16803.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,7 @@ Module Test2.
6565
exact I.
6666
Defined.
6767

68-
Fail Constraint mkrel.u0 < unZ2.u.
68+
Fail Constraint mkrel.u0 < Z2.u.
6969

7070
End Test2.
7171

@@ -92,7 +92,7 @@ Module Test3.
9292
}.
9393
Add Zify BinRel Op_eq.
9494

95-
Constraint mkrel.u0 < unZ2.u.
95+
Constraint mkrel.u0 < Z2.u.
9696

9797
Theorem lia_refl_ex : forall (a b : Z2), a = a.
9898
Proof.

0 commit comments

Comments
 (0)