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