| Commit message (Expand) | Author | Age |
* | Haskell extraction: use explicit -XMagicHash instead of -fglasgow-exts | Nickolai Zeldovich | 2014-10-28 |
* | Haskell extraction: put unsafeCoerce type declaration later | Nickolai Zeldovich | 2014-10-28 |
* | Fix some typos in comments. | Guillaume Melquiond | 2014-10-27 |
* | library/opaqueTables: enable their use in interactive mode | Enrico Tassi | 2014-10-13 |
* | Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name | Matthieu Sozeau | 2014-10-11 |
* | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | 2014-09-27 |
* | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack | 2014-09-04 |
* | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau | 2014-08-28 |
* | "allows to", like "allowing to", is improper | Jason Gross | 2014-08-25 |
* | instanciation is French, instantiation is English | Jason Gross | 2014-08-25 |
* | Grammar: "allowing to" is not proper English | Jason Gross | 2014-08-25 |
* | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin | 2014-08-01 |
* | Deprecate options -dont, -lazy, -force-load-proofs. | Guillaume Melquiond | 2014-06-13 |
* | Reuse universe level substitutions for template polymorphism, fixing performance | Matthieu Sozeau | 2014-05-09 |
* | Fix extraction taking a type in the wrong environment. | Matthieu Sozeau | 2014-05-06 |
* | Fix a pervasive equality use. | Matthieu Sozeau | 2014-05-06 |
* | - Rename eq to equal in Univ, document new modules, set interfaces. | 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-05-06 |
* | Using HMaps in global references. | Pierre-Marie Pédrot | 2014-03-08 |
* | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey | 2014-03-05 |
* | Fixing Pervasives.equality in extraction. | Pierre-Marie Pédrot | 2014-03-03 |
* | Lazyconstr -> Opaqueproof | Enrico Tassi | 2014-02-26 |
* | New compilation mode -vi2vo | Enrico Tassi | 2014-02-26 |
* | More monomorphic List.mem + List.assoc + ... | letouzey | 2013-10-24 |
* | Turn many List.assoc into List.assoc_f | letouzey | 2013-10-24 |
* | cList.index is now cList.index_f, same for index0 | letouzey | 2013-10-23 |
* | Removing a bunch of generic equalities. | ppedrot | 2013-09-27 |
* | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc | 2013-09-19 |
* | Nicer code concerning dirpaths and modpath around Lib | letouzey | 2013-08-22 |
* | Declarations.mli: reorganization of modular structures | letouzey | 2013-08-20 |
* | Vernac classification streamlined (handles VERNAC EXTEND) | gareuselesinge | 2013-08-08 |
* | State Transaction Machine | gareuselesinge | 2013-08-08 |
* | Lib.contents () instead of Lib.contents_after None | letouzey | 2013-07-17 |
* | Extraction : message about lack of support for toplevel Include | letouzey | 2013-07-17 |
* | bwaa, a Pervasive.compare | pboutill | 2013-05-30 |
* | Removing Gmap from Extraction plugin | ppedrot | 2013-05-12 |
* | Use the Hook module here and there. | ppedrot | 2013-05-12 |
* | Splitting Term into five unrelated interfaces: | ppedrot | 2013-04-29 |
* | code simplifications concerning Summary | letouzey | 2013-04-22 |
* | Extraction AccessOpaque is now activated again by default (#2952) | letouzey | 2013-03-18 |
* | Extract_env : correct exceptions mentionned in a try ... with | letouzey | 2013-03-15 |
* | 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-03-13 |
* | kernel/declarations becomes a pure mli | letouzey | 2013-02-26 |
* | Names: shortcuts for building {kn, constant, mind} with empty sections | letouzey | 2013-02-26 |
* | Names: Modularize constant and mutual_inductive | letouzey | 2013-02-26 |
* | Dir_path --> DirPath | letouzey | 2013-02-19 |
* | Classops : avoid some use of Gmap | letouzey | 2013-02-19 |
* | use List.rev_map whenever possible | letouzey | 2013-02-18 |