aboutsummaryrefslogtreecommitdiff
path: root/tactics/abstract.ml
AgeCommit message (Collapse)Author
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :)
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-10-30Move abstract out of tactics.mlGaëtan Gilbert