path: root/test-suite/success/Section.v

(* Test bug 2168: ending section of some name was removing objects of the
   same name *)

Require Import make_notation.

Check add2 3.