blob: 22a075e0965ad5b060504be651184c65beb5f82b (
plain)
1
2
3
4
5
6
7
8
9
10
|
(* Ensure that evars are properly normalized in the instance path.
Problems with this can cause eg #11161. *)
Class Foo (n:nat) := {x : bool}.
Instance bar n : Foo n. Admitted.
Instance bar' n : Foo n. split. abstract exact true. Qed.
Instance bar'' n : Foo n. split. abstract exact true. Defined.
|
