aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.ml
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Universes algorithm : clarified commentsGravatar Jacques-Henri Jourdan2016-01-17
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-29
|\|
| * Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
| * Fix output of universe arcs. (Fix bug #4422)Gravatar Guillaume Melquiond2015-11-23
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\|
| * Univs: update refman, better printers for universe contexts.Gravatar Matthieu Sozeau2015-11-04
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\|
| * Adds support for the virtual machine to perform reduction of universe polymor...Gravatar Gregory Malecha2015-10-28
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|\|
| * Univs: fix bug #3807Gravatar Matthieu Sozeau2015-10-08
* | Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
|/
* Univs: fix bug #4288, Print Sorted generated backward < constraints.Gravatar Matthieu Sozeau2015-10-05
* Univs: fix bug #4251, handling of template polymorphic constants.Gravatar Matthieu Sozeau2015-10-02
* Univs (kernel) adapt to new invariantsGravatar Matthieu Sozeau2015-10-02
* Forcing i > Set for global universes (incomplete)Gravatar Matthieu Sozeau2015-10-02
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2015-08-02
* Modules: fix bug #4294Gravatar Matthieu Sozeau2015-07-16
* Further simplification of the graph traversal in Univ.Gravatar Pierre-Marie Pédrot2015-07-01
* Less closures makes the GC happy.Gravatar Pierre-Marie Pédrot2015-06-24
* Less closures makes the GC happy.Gravatar Pierre-Marie Pédrot2015-06-23
* Fixing bug #4019, and checker blow-up at once.Gravatar Pierre-Marie Pédrot2015-02-11
* Clarifying the implementation of universe hashconsing.Gravatar Pierre-Marie Pédrot2015-02-11
* Fixing bug #3931.Gravatar Pierre-Marie Pédrot2015-01-28
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* Aligning printing of universe constraints.Gravatar Hugo Herbelin2015-01-07
* Dead code in Univ.Gravatar Pierre-Marie Pédrot2014-12-21
* Cleaning up universe list implementation in Univ.Gravatar Pierre-Marie Pédrot2014-12-18
* Ensuring the good invariants of hashcons table generation in the API.Gravatar Pierre-Marie Pédrot2014-12-17
* Fix merging of name maps in union of universe contexts.Gravatar Matthieu Sozeau2014-12-14
* Implement module subtyping for polymorphic constants (errors onGravatar Matthieu Sozeau2014-10-02
* Clean a bit of univ.ml, add credits.Gravatar Matthieu Sozeau2014-09-18
* Fix checker treatment of inductives using subst_instances instead of subst_un...Gravatar Matthieu Sozeau2014-09-05
* Fix bug #3559, ensuring a canonical order of universe level quantifications whenGravatar Matthieu Sozeau2014-09-04
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was larger...Gravatar Matthieu Sozeau2014-08-18
* Adding a primitive to merge ContextSets which is more efficient when oneGravatar Pierre-Marie Pédrot2014-08-09
* Cleaning up interface of ContextSet.Gravatar Pierre-Marie Pédrot2014-08-09
* Fixing semantics of Univ.Level.equal.Gravatar Pierre-Marie Pédrot2014-08-04
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* Useless export of Instance.eqeq. We hashcons everything before calling thisGravatar Pierre-Marie Pédrot2014-07-31
* Avoid hconsing instances during appends and conversions from/to arrays.Gravatar Matthieu Sozeau2014-07-30
* Universe level maps use HMaps.Gravatar Pierre-Marie Pédrot2014-07-21
* Cleanup substitution inside universe instances, only done through subst_fn now,Gravatar Matthieu Sozeau2014-07-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-05 03:01:33 +0000