aboutsummaryrefslogtreecommitdiff
path: root/tactics/proof_global.ml
AgeCommit message (Expand)Author
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