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

summary refs log tree commit diff

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

blob: 99da1e3e4489e239d80e6524c15b5e08d318d144 (plain)

Require Import Program.

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