summaryrefslogtreecommitdiff
path: root/test-suite/success/Remark.v
blob: 2dd6a2113eeef7ba3e37fcc7e7d92c424e40d5bb (plain)
1
2
3
4
5
6
7
8
9
10
11
12
(* 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.
*)