aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacsubst.ml
AgeCommit message (Expand)Author
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-21Yet a new reduction tactic in Coq : cbnpboutill
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
2012-11-25Monomorphization (tactics)ppedrot
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey