aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/g_indfun.ml4
AgeCommit message (Expand)Author
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-02Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codePierre Letouzey
2014-02-16Removing non-marshallable data from the Agram constructor. Instead ofPierre-Marie Pédrot
2013-12-04Vernac classification: allow for commands which start proofs but must be sync...Arnaud Spiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-08-08Vernac classification streamlined (handles VERNAC EXTEND)gareuselesinge
2013-06-21Cutting the dependency of Genarg in constr_expr, glob_constrppedrot
2013-06-06Uniformizing generic argument types.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 9)letouzey
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-08-08Updating headers.herbelin
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-10 12:44:13 +0000