aboutsummaryrefslogtreecommitdiff
path: root/tactics/abstract.ml
AgeCommit message (Expand)Author
2019-05-24Fixing typosJPR
2019-05-23Fixing typos - Part 3JPR
2019-05-19Merge the definition of constants and private constants in the API.Pierre-Marie Pédrot
2019-05-15Simplify the private constant API.Pierre-Marie Pédrot
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-12[tactics] Remove dependency of abstract on global proof state.Emilio Jesus Gallego Arias
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-10-30Move abstract out of tactics.mlGaëtan Gilbert