(* Test obsolete, Remark est maintenant global Section A. Section B. Section C. Remark t : True. Proof I. End C. Locate C.t. End B. Locate B.C.t. End A. Locate A.B.C.t. *)