diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/2375.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2375.v | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2375.v b/test-suite/bugs/closed/shouldsucceed/2375.v deleted file mode 100644 index c17c426c..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2375.v +++ /dev/null @@ -1,18 +0,0 @@ -(* In the following code, the (superfluous) lemma [lem] is responsible -for the failure of congruence. *) - -Definition f : nat -> Prop := fun x => True. - -Lemma lem : forall x, (True -> True) = ( True -> f x). -Proof. - intros. reflexivity. -Qed. - -Goal forall (x:nat), x = x. -Proof. - intros. - assert (lem := lem). - (*clear ax.*) - congruence. -Qed. - |