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

summary refs log tree commit diff

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

blob: 900bfc34b37f1c1c4af5018a9707bd7c8ca9f13c (plain)

Module foo.
  Notation x := $(exact I)$.
End foo.
Module bar.
  Fail Include foo.
End bar.