univ_constraints_statements_body.v « vio « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/vio/univ_constraints_statements_body.v

blob: 6302adefc2f167c0c34ce6deee88afe624ac0892 (plain)

Definition T := Type.
Definition T1 : T := Type.

Lemma x : True.
Proof.
exact (let a : T := Type in I).
Qed.