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

Require Import make_notation.

Check add2 3.