aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacsubst.ml
Commit message (Expand)AuthorAge
* Uniformizing generic argument types.Gravatar ppedrot2013-06-06
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* 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
* Moved Stringset and Stringmap to String namespace.Gravatar ppedrot2012-12-14
* Monomorphization (tactics)Gravatar ppedrot2012-11-25
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16