aboutsummaryrefslogtreecommitdiff
path: root/tactics/taccoerce.ml
AgeCommit message (Expand)Author
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-07-05Expurgating the useless difference between List0 and List1 at theppedrot
2013-06-27Removed the distinction between generic Ltac vars and Let/Introppedrot
2013-06-21Cutting the dependency of Genarg in constr_expr, glob_constrppedrot
2013-06-19Moving wit_unit to Stdarg.ppedrot
2013-06-18Proof-of-concept: moved four easy-to-handle generic arguments toppedrot
2013-06-13Normalizing exception raised by tactic coercions.ppedrot
2013-06-12Moving coercion functions out of Tacinterp.ppedrot