blob: 9625af91f5ccdc2b96713e4c33cde9503cd7456c (
plain)
1
2
3
4
5
6
7
|
(* Was an anomaly with ill-typed template polymorphism *)
Definition huh (b:bool) := if b then Set else Prop.
Definition lol b: huh b :=
if b return huh b then nat else True.
Goal (lol true) * unit.
Fail generalize true. (* should fail with error, not anomaly *)
Abort.
|
