2814.v « opened « bugs « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/test-suite/bugs/opened/2814.v

blob: a740b4384d42c1becc0c760ca6b3c7816da4dff8 (plain)

Require Import Program.

Goal forall (x : Type) (f g : Type -> Type) (H : f x ~= g x), False.
  intros.
  Fail induction H.