aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_001.v
blob: bf1d024b2ee19c0c55c66e3b8a90e43afefaa076 (plain)
1
2
3
4
5
Record Foo : Set :=
  {
    A' : nat;
    A : Prop := (A' = 0)
  }. (* Anomaly: Uncaught exception Reduction.NotConvertible. Please report. *)