aboutsummaryrefslogtreecommitdiff
path: root/tactics/proof_global.mli
AgeCommit message (Expand)Author
2019-11-08Make [Proof_global.closed_proof_output] opaqueGaëtan Gilbert
2019-10-04Remove redundancy in section hypotheses of kernel entries.Pierre-Marie Pédrot
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on top...Emilio Jesus Gallego Arias