| Age | Commit message (Expand) | Author |
|---|
| 2014-12-16 | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot |
| 2014-11-27 | Reverting the following block of three commits: | Hugo Herbelin |
| 2014-11-26 | Registering strict implicit arguments systematically. | Hugo Herbelin |
| 2014-09-27 | Keyed unification option, compiling the whole standard library | Matthieu Sozeau |
| 2014-09-10 | Parsing and printing of primitive projections, fix buggy behavior when | Matthieu Sozeau |
| 2014-09-09 | - Fix printing and parsing of primitive projections, including the Set | Matthieu Sozeau |
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-17 | - Fix the de Bruijn problem in check_projection for good :) | Matthieu Sozeau |
| 2014-05-06 | Fix printing of projections with implicits. | Matthieu Sozeau |
| 2014-05-06 | Initial work on reintroducing old-style polymorphism for compatibility (the s... | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-02 | Fix Bug 3217 | Pierre Boutillier |
| 2014-03-01 | Fixing pervasive comparisons | Pierre-Marie Pédrot |
| 2013-10-24 | Turn many List.assoc into List.assoc_f | letouzey |
| 2013-09-19 | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc |
| 2013-04-22 | code simplifications concerning Summary | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 8) | letouzey |
| 2013-01-28 | Actually adding backtrace handling. | ppedrot |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-22 | Monomorphization (library) | ppedrot |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-03-20 | Fixing alpha-conversion bug #2723 introduced in r12485-12486. | herbelin |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-12-18 | Fixed a Not_found bug when declaring in a section some implicit | herbelin |
| 2011-12-06 | Minor fixes to Arguments | gareuselesinge |
| 2011-11-21 | Renamig support added to "Arguments" | gareuselesinge |
| 2011-11-21 | New Arguments vernacular | gareuselesinge |
| 2011-11-02 | Add type annotations around all calls to Libobject.declare_object | letouzey |
| 2011-04-03 | Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks | letouzey |
| 2011-02-10 | More comments and less doublons in some mli | pboutill |
| 2010-10-05 | Export definition of type implicits_list for contribs + fixed a | herbelin |
| 2010-10-04 | Fixing bugs in previous commits about implicit arguments: | herbelin |
| 2010-10-03 | Added multiple implicit arguments rules per name. | herbelin |
| 2010-10-03 | Dead code in impargs (afaics, no more need, since r11242, to merge | herbelin |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-16 | Util: remove list_split_at which is a clone of list_chop | letouzey |
| 2009-12-01 | Continuing r12485-12486 (cleaning around name generation) | herbelin |
| 2009-11-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin |
