diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4069.v | 16 |
2 files changed, 16 insertions, 1 deletions
@@ -24,6 +24,7 @@ Other bugfixes - #4882: anomaly with Declare Implicit Tactic on hole of type with evars - Fix use of "Declare Implicit Tactic" in refine. triggered by CoqIDE +- #4069, #4718: congruence fails when universes are involved. Universes - Disallow silently dropping universe instances applied to variables diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v index 11289f7575..61527764e2 100644 --- a/test-suite/bugs/closed/4069.v +++ b/test-suite/bugs/closed/4069.v @@ -87,4 +87,18 @@ f_equal. Undo 2. unshelve refine (tequator (X _)); revgoals. f_equal. -Admitted.
\ No newline at end of file +Admitted. + +Goal @eq Set nat nat. +congruence. +Qed. + +Goal @eq Type nat nat. +congruence. +Qed. + +Variable T : Type. + +Goal @eq Type T T. +congruence. +Qed.
\ No newline at end of file |