| Age | Commit message (Expand) | Author |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2014-03-03 | Fixing Pervasives.equality in extraction. | Pierre-Marie Pédrot |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-09-27 | Removing a bunch of generic equalities. | ppedrot |
| 2013-09-19 | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc |
| 2013-08-22 | Nicer code concerning dirpaths and modpath around Lib | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 6) | letouzey |
| 2013-02-26 | kernel/declarations becomes a pure mli | letouzey |
| 2013-02-26 | Names: shortcuts for building {kn, constant, mind} with empty sections | letouzey |
| 2013-02-19 | Dir_path --> DirPath | letouzey |
| 2012-12-18 | Modulification of Label | ppedrot |
| 2012-12-14 | Modulification of dir_path | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-12-14 | Moved Intset and Intmap to Int namespace. | ppedrot |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-15 | Some documentation and cleaning of CList and Util interfaces. | ppedrot |
| 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-24 | Add option Set/Unset Extraction Conservative Types. | aspiwack |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-12-10 | Extraction: only do the test on generalizable lets for ocaml | letouzey |
| 2011-12-08 | Extraction: avoid internal eta-reduction (fix #2570) | letouzey |
| 2011-11-29 | Extraction: typo in last commit | letouzey |
| 2011-11-28 | Extraction: Richer patterns in matchs as proposed by P.N. Tollitte | letouzey |
| 2011-07-04 | Extraction: in haskell, __ may have any type, no need to unsafeCoerce it | letouzey |
| 2011-04-07 | Extraction: unfolds the let-in created by Program when handling "match" | letouzey |
| 2011-04-07 | Extraction: avoid some useless Obj.magic by fixing my ML type unifier | letouzey |
| 2011-04-03 | Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks | letouzey |
| 2010-12-21 | Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413) | letouzey |
| 2010-09-24 | Dead code in extraction | letouzey |
| 2010-09-17 | Extraction: multiple fixes related with the Not_found encountered by X. Leroy | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-07-08 | Extraction: restrict autoinling to csts whose body is globally visible (fix #... | letouzey |
| 2010-07-08 | Extraction: more factorization of common match branches | letouzey |
| 2010-07-08 | Extraction: Unset Extraction AutoInline is now the default | letouzey |
| 2010-06-16 | Extraction: fix the eta reduction function used in code optimisations | letouzey |
| 2010-06-08 | Extraction with implicits: perform the occur-check after optimisations | letouzey |
| 2010-05-01 | Extraction: fix type_expunge_from_sign broken in last commit | letouzey |
| 2010-04-30 | Extraction: an experimental command to get rid of some cst/constructor arguments | letouzey |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-16 | Extraction: restore (temporarily?) a very limited form of linear letin reduction | letouzey |
| 2010-04-16 | Extraction: less eta in calls to global functions, better optimization phase | letouzey |
| 2010-04-16 | Extraction: improvement of optimizations (kill_dummy, optim_fix) | letouzey |
| 2010-04-16 | Extraction: ad-hoc identifier type with annotations for reductions | letouzey |
| 2010-04-16 | Extraction: less _ in Haskell (typically for False_rect), less toplevel eta-e... | letouzey |