aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.ml
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Simplify Univ.mlGravatar Amin Timany2017-06-16
* Squashed commit of the following:Gravatar Amin Timany2017-06-16
* Check subtyping of inductive types in KernelGravatar Amin Timany2017-06-16
* Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
* New datastructure for universes of inductive typesGravatar Amin Timany2017-06-16
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* Document changesGravatar Matthieu Sozeau2016-12-02
* Slightly more efficient [Univ.super] implemGravatar Matthieu Sozeau2016-11-30
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\
| * A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2016-03-22
* | 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