aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/g_indfun.ml4
Commit message (Expand)AuthorAge
* place all files specific to camlp4 syntax extensions in grammar/Gravatar letouzey2012-05-29
* slim down a bit genarg.ml (pr_intro_pattern forgotten there)Gravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Fixing bug #2732 (anomaly when using the tolerance for writingGravatar herbelin2012-03-18
* Noise for nothingGravatar pboutill2012-03-02
* Call process_vernac_interp_error before calling Errors.print inGravatar herbelin2011-06-10
* A new mechanism to handle errors.Gravatar aspiwack2011-05-13
* ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPEDGravatar glondu2010-12-25
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesGravatar glondu2010-09-30
* Report fix bug 2345 from v8.3 (Bad error message when functionalGravatar courtieu2010-09-21
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* Using vernac parsing for FunctionGravatar jforest2010-06-08
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 11:01:41 +0000