aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/g_indfun.ml4
AgeCommit message (Expand)Author
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
2012-05-29slim down a bit genarg.ml (pr_intro_pattern forgotten there)letouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-18Fixing bug #2732 (anomaly when using the tolerance for writingherbelin
2012-03-02Noise for nothingpboutill
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-02-26 18:06:14 +0000