aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/g_indfun.ml4
AgeCommit message (Expand)Author
2011-06-10Call process_vernac_interp_error before calling Errors.print inherbelin
2011-05-13A new mechanism to handle errors.aspiwack
2010-12-25ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPEDglondu
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-09-30Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesglondu
2010-09-21Report fix bug 2345 from v8.3 (Bad error message when functionalcourtieu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
2010-06-08Using vernac parsing for Functionjforest
2009-12-21Generic support for open terms in tacticsherbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 21:15:47 +0000