| Age | Commit message (Expand) | Author |
|---|
| 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-13 | Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284). | Hugo Herbelin |
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau |
| 2014-05-06 | - 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-04-09 | 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-03-14 | Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had | Pierre-Marie Pédrot |
| 2014-03-07 | Using Hashmaps by default in constant and inductive maps. This changes fold and | Pierre-Marie Pédrot |
| 2014-03-06 | Inductive maps in Environ now use HMap. | Pierre-Marie Pédrot |
| 2014-03-05 | Using HMaps in Safe_env.environments, hopefully improving performances. | Pierre-Marie Pédrot |
| 2014-02-26 | Lazyconstr -> Opaqueproof | Enrico Tassi |
| 2014-02-03 | Tracking memory misallocation by trying to improve sharing. | Pierre-Marie Pédrot |
| 2014-01-05 | Environ: export API to transitively close a set of section variables | Enrico Tassi |
| 2013-12-28 | Removing native_name reference from constant_body. | Maxime Dénès |
| 2013-11-15 | Revert "Fast lookup_named in environments, based on maps instead of lists." | ppedrot |
| 2013-11-13 | Fast lookup_named in environments, based on maps instead of lists. | ppedrot |
| 2013-10-31 | Conv_orable made functional and part of pre_env | gareuselesinge |
| 2013-10-22 | Removing some generic equalities. | ppedrot |
| 2013-08-25 | Replacing lists by sets in clear tactic. | ppedrot |
| 2013-08-20 | Safe_typing code refactoring | letouzey |
| 2013-04-29 | Merging Context and Sign. | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-02-26 | kernel/declarations becomes a pure mli | letouzey |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-13 | More monomorphizations | ppedrot |
| 2012-11-08 | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot |
| 2012-09-14 | 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-08-11 | fast bitwise operations (lor,land,lxor) on int31 and BigN | letouzey |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-03-14 | Final part of moving Program code inside the main code. Adapted add_definitio... | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-10-26 | When checking for emptiness, use Foo.is_empty instead of (=) Foo.empty | letouzey |
| 2011-10-26 | Environ.set_universes is dead code | letouzey |
| 2011-10-25 | First attempt at making Print Assumption compatible with opaque modules (fix ... | letouzey |
| 2011-07-29 | Environ: generic equality on named_context replaced by named_context_equal | puech |
| 2011-04-03 | Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks | letouzey |
| 2010-12-18 | Univ.constraints made fully abstract instead of being a Set of abstract stuff | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-05-09 | Added a few informations about file lineages (for the most part in kernel) | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
