| Age | Commit message (Expand) | Author |
|---|
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 9) | 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-18 | Extraction: same as commit 16203, hopefully without NotASort exns | letouzey |
| 2013-02-14 | Fix extraction of inductive types that Coq auto-detects to be in Prop | letouzey |
| 2012-12-18 | Modulification of Label | ppedrot |
| 2012-12-17 | Extraction of projections: restrict a hack to ocaml only (fix #2941) | letouzey |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-12-14 | Moved Intset and Intmap to Int namespace. | ppedrot |
| 2012-10-30 | Extraction Implicit: consider the parameters of a constructor (fix #2905) | letouzey |
| 2012-09-18 | Cleaning interface of Util. | 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 | Fix Extraction Implicit on axioms. | 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-30 | Extraction: try to avoid issues with an Include directly inside a .v | letouzey |
| 2011-11-28 | Extraction: Richer patterns in matchs as proposed by P.N. Tollitte | letouzey |
| 2011-09-05 | Extraction Implicit: fix the numbering of constructor arguments | letouzey |
| 2011-08-25 | Extraction: allow extraction of records with anonymous fields (fix #2555) | letouzey |
| 2011-07-29 | Extraction: replace generic = on mutual_inductive_body by mib_equal | puech |
| 2011-07-04 | Set Extraction KeepSingleton: an option for not decapsulating singleton types | letouzey |
| 2011-07-04 | Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml | letouzey |
| 2011-04-13 | Extraction: opaque terms are not traversed anymore by default | letouzey |
| 2011-04-03 | Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks | letouzey |
| 2011-03-31 | Extraction: customized inductives are always standard | glondu |
| 2011-03-07 | Extraction: a warning when an opaque constant is enterred | 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-20 | Extraction: re-introduce some eta-expansions in rare situations leading to '_... | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-07-08 | Extraction: more factorization of common match branches | 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: less eta in calls to global functions, better optimization phase | letouzey |
| 2010-04-16 | Util: remove list_split_at which is a clone of list_chop | 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 |
| 2009-11-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin |
| 2009-10-21 | This big commit addresses two problems: | soubiran |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-03-20 | Directory 'contrib' renamed into 'plugins', to end confusion with archive of ... | letouzey |
