aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Section.v
blob: 8e9e79b3e53d15520dfdc58cee307147a7611bd2 (plain)
1
2
3
4
5
6
(* Test bug 2168: ending section of some name was removing objects of the
   same name *)

Require Import make_notation.

Check add2 3.