aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/taccoerce.ml
Commit message (Expand)AuthorAge
* Expurgating the useless difference between List0 and List1 at theGravatar ppedrot2013-07-05
* Removed the distinction between generic Ltac vars and Let/IntroGravatar ppedrot2013-06-27
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Moving wit_unit to Stdarg.Gravatar ppedrot2013-06-19
* Proof-of-concept: moved four easy-to-handle generic arguments toGravatar ppedrot2013-06-18
* Normalizing exception raised by tactic coercions.Gravatar ppedrot2013-06-13
* Moving coercion functions out of Tacinterp.Gravatar ppedrot2013-06-12