aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/g_class.ml4
Commit message (Expand)AuthorAge
* Update headers.Gravatar Maxime Dénès2015-01-12
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Splitting Class_tactics between code and CAMLP4/5 declarations.Gravatar ppedrot2013-10-04