aboutsummaryrefslogtreecommitdiff
path: root/tactics/abstract.mli
AgeCommit message (Expand)Author
2020-04-21[declare] [tactics] Move declare to `vernac`Emilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-10-29[declare] Make `proof_entry` a private type.Emilio Jesus Gallego Arias
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on top...Emilio Jesus Gallego Arias
2019-06-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
2019-06-20Merge PR #9645: [proof] Remove terminator type, unifying regular and obligati...Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17[equations] [proof] Remove duplicate shrink function.Emilio Jesus Gallego Arias
2019-02-12[tactics] Remove dependency of abstract on global proof state.Emilio Jesus Gallego Arias
2018-10-30Move abstract out of tactics.mlGaëtan Gilbert