3093.v « closed « bugs « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

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

blob: f6b4a03f3b6348740db07d827badecc32cb5c1e7 (plain)

Require Import FunctionalExtensionality.

Goal forall y, @f_equal = y.
  intro.
  apply functional_extensionality_dep.
Abort.