| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | Reverting 16 last commits, committed mistakenly using the wrong push command. |  Hugo Herbelin | 2015-08-02 |
| * | Fixing pop_rel_context | Hugo Herbelin | 2015-08-02 |
| * | Option -type-in-type: added support in checker and making it contaminating | Hugo Herbelin | 2015-07-10 |
| * | Fix vm compiler to refuse to compile code making use of inductives with |  Matthieu Sozeau | 2015-03-25 |
| * | Correct restriction of vm_compute when handling universe polymorphic |  Matthieu Sozeau | 2015-01-15 |
| * | Update headers. |  Maxime Dénès | 2015-01-12 |
| * | Declarations.mli refactoring: module_type_body = module_body |  Pierre Letouzey | 2015-01-11 |
| * | Cleaner interfaces for linking locations of native compiler. | Maxime Dénès | 2014-11-12 |
| * | Fix retroknowledge for int31 division. | Maxime Dénès | 2014-10-24 |
| * | library/opaqueTables: enable their use in interactive mode |  Enrico Tassi | 2014-10-13 |
| * | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | 2014-09-27 |
| * | Make the retroknowledge marshalable. |  Arnaud Spiwack | 2014-09-24 |
| * | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin | 2014-09-13 |
| * | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau | 2014-08-03 |
| * | Removing dead code. |  Pierre-Marie Pédrot | 2014-06-17 |
| * | Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284). | Hugo Herbelin | 2014-06-13 |
| * | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau | 2014-06-04 |
| * | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | 2014-05-06 |
| * | Adapt universe polymorphic branch to new handling of futures for delayed proofs. | Matthieu Sozeau | 2014-05-06 |
| * | - Rename eq to equal in Univ, document new modules, set interfaces. | Matthieu Sozeau | 2014-05-06 |
| * | Fix interface for template polymorphism, cleaning up code in all typing algor... | 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 |
| * | Int31 decompilation in native compiler was still partial. Now fixed. | Maxime Dénès | 2014-04-09 |
| * | Machine arithmetic operations for native compiler. | Maxime Dénès | 2014-04-09 |
| * | Full support for int31 values in native compiler. | Maxime Dénès | 2014-04-09 |
| * | Partial support for open terms in int31. | Maxime Dénès | 2014-04-09 |
| * | Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had | Pierre-Marie Pédrot | 2014-03-14 |
| * | Using Hashmaps by default in constant and inductive maps. This changes fold and | Pierre-Marie Pédrot | 2014-03-07 |
| * | Inductive maps in Environ now use HMap. | Pierre-Marie Pédrot | 2014-03-06 |
| * | Using HMaps in Safe_env.environments, hopefully improving performances. | Pierre-Marie Pédrot | 2014-03-05 |
| * | Lazyconstr -> Opaqueproof | Enrico Tassi | 2014-02-26 |
| * | Tracking memory misallocation by trying to improve sharing. | Pierre-Marie Pédrot | 2014-02-03 |
| * | Environ: export API to transitively close a set of section variables | Enrico Tassi | 2014-01-05 |
| * | Removing native_name reference from constant_body. | Maxime Dénès | 2013-12-28 |
| * | Revert "Fast lookup_named in environments, based on maps instead of lists." |  ppedrot | 2013-11-15 |
| * | Fast lookup_named in environments, based on maps instead of lists. | ppedrot | 2013-11-13 |
| * | Conv_orable made functional and part of pre_env |  gareuselesinge | 2013-10-31 |
| * | Removing some generic equalities. | ppedrot | 2013-10-22 |
| * | Replacing lists by sets in clear tactic. | ppedrot | 2013-08-25 |
| * | Safe_typing code refactoring |  letouzey | 2013-08-20 |
| * | Merging Context and Sign. | ppedrot | 2013-04-29 |
| * | Splitting Term into five unrelated interfaces: | ppedrot | 2013-04-29 |
| * | kernel/declarations becomes a pure mli | letouzey | 2013-02-26 |
| * | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
| * | Modulification of identifier | ppedrot | 2012-12-14 |
| * | More monomorphizations | ppedrot | 2012-11-13 |
| * | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot | 2012-11-08 |
| * | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot | 2012-09-14 |
| * | The new ocaml compiler (4.00) has a lot of very cool warnings, |  regisgia | 2012-09-14 |
Hugo Herbelin
Matthieu Sozeau
Matthieu Sozeau
Maxime Dénès
Pierre Letouzey
Enrico Tassi
Arnaud Spiwack
Pierre-Marie Pédrot
ppedrot
gareuselesinge
letouzey
regisgia