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

summary refs log tree commit diff

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.