aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacintern.ml
Commit message (Expand)AuthorAge
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Yet a new reduction tactic in Coq : cbnGravatar pboutill2012-12-21
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Moved Stringset and Stringmap to String namespace.Gravatar ppedrot2012-12-14
* Monomorphization (tactics)Gravatar ppedrot2012-11-25
* Taking into account the type of a definition (if it exists), and theGravatar herbelin2012-11-17
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16