blob: c4b29a6354cb66a98d5c398c68e4e9b3d2de1769 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(* Check that instances for local definitions in evars have compatible body *)
Goal False.
Proof.
pose (n := 1).
evar (m:nat).
subst n.
pose (n := 0).
Fail Check ?m. (* n cannot be reinterpreted with a value convertible to 1 *)
clearbody n.
Fail Check ?m. (* n cannot be reinterpreted with a value convertible to 1 *)
clear n.
pose (n := 0+1).
Check ?m. (* Should be ok *)
Abort.
|
