DEBSOURCES
Skip Quicknav
sources / coq / 9.1.0%2Bdfsg-3 / test-suite / bugs / bug_1547.v
12345
(* Compatibility of Require with backtracking at interactive module end *) Module A. Require ListDef. End A.