| Age | Commit message (Expand) | Author |
|---|
| 2015-10-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-28 | Adds support for the virtual machine to perform reduction of universe polymor... | Gregory Malecha |
| 2015-10-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-08 | Univs: fix bug #3807 | Matthieu Sozeau |
| 2015-10-06 | Splitting kernel universe code in two modules. | Pierre-Marie Pédrot |
| 2015-10-02 | Univs: fix bug #4251, handling of template polymorphic constants. | Matthieu Sozeau |
| 2015-10-02 | Univs (kernel) adapt to new invariants | Matthieu Sozeau |
| 2015-10-02 | Forcing i > Set for global universes (incomplete) | Matthieu Sozeau |
| 2015-10-02 | Universes: enforce Set <= i for all Type occurrences. | Matthieu Sozeau |
| 2015-01-17 | Univs: proper printing of global and local universe names (only | Matthieu Sozeau |
| 2015-01-17 | Make native compiler handle universe polymorphic definitions. | Maxime Dénès |
| 2015-01-15 | Correct restriction of vm_compute when handling universe polymorphic | Matthieu Sozeau |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-10-02 | Implement module subtyping for polymorphic constants (errors on | Matthieu Sozeau |
| 2014-08-30 | Simplify even further the declaration of primitive projections, | Matthieu Sozeau |
| 2014-08-09 | Adding a primitive to merge ContextSets which is more efficient when one | Pierre-Marie Pédrot |
| 2014-08-09 | Cleaning up interface of ContextSet. | Pierre-Marie Pédrot |
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-07-31 | Useless export of Instance.eqeq. We hashcons everything before calling this | Pierre-Marie Pédrot |
| 2014-07-21 | Universe level maps use HMaps. | Pierre-Marie Pédrot |
| 2014-07-21 | Cleanup substitution inside universe instances, only done through subst_fn now, | Matthieu Sozeau |
| 2014-07-03 | Cleanup code related to the constraint solving, which sits now outside the | Matthieu Sozeau |
| 2014-07-01 | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau |
| 2014-06-18 | Code factorization in LMap. | Pierre-Marie Pédrot |
| 2014-06-10 | Made explanations for universe inconsistencies optional. They are only used | Pierre-Marie Pédrot |
| 2014-06-10 | - Fix substitution of universes which needlessly hashconsed existing universes. | Matthieu Sozeau |
| 2014-06-10 | More cleanup/reorganizing of univ.ml to separate constraint/universe handling... | Matthieu Sozeau |
| 2014-06-10 | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau |
| 2014-06-10 | Remove unused function in univ | Matthieu Sozeau |
| 2014-06-08 | Function in Univ uselessly exported. | Pierre-Marie Pédrot |
| 2014-06-04 | - Force every universe level to be >= Prop, so one cannot "go under" it anymore. | Matthieu Sozeau |
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau |
| 2014-05-06 | Find a more efficient fix for dealing with template universes: | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | - Fix handling of polymorphic inductive elimination schemes. | Matthieu Sozeau |
| 2014-05-06 | - Rename eq to equal in Univ, document new modules, set interfaces. | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-03-03 | Fixing Pervasives.equality in extraction. | Pierre-Marie Pédrot |
| 2013-10-24 | Specializing hash functions for widely used types. | ppedrot |
| 2013-08-20 | Universe counters on slaves are in sync with master | gareuselesinge |
| 2013-03-12 | A version of Univ.check_eq with no anomaly for Evd.set_eq_sort | letouzey |
| 2013-02-19 | Dir_path --> DirPath | letouzey |
| 2012-12-14 | Modulification of dir_path | ppedrot |
| 2012-11-26 | Small cleaning of interface in Univ | ppedrot |
| 2012-10-17 | univ inconsistency error message gives evidence of a cycle | barras |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-03-22 | Univ: enforce_leq instead of enforce_geq for more uniformity | letouzey |
| 2012-03-01 | Univ: a univ_depends function to avoid a hack in Inductiveops | letouzey |
| 2011-10-26 | When checking for emptiness, use Foo.is_empty instead of (=) Foo.empty | letouzey |
| 2011-10-10 | Hash-consing of mutual_inductive_body (and Univ.constraints) | letouzey |
