aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/qed_export.v
AgeCommit message (Expand)Author
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
2015-03-22Qed export -> Qed exportingEnrico Tassi
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi