index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
univ.ml
Commit message (
Expand
)
Author
Age
*
Collecting List.smart_* functions into a module List.Smart.
Hugo Herbelin
2018-05-23
*
Collecting Array.smart_* functions into a module Array.Smart.
Hugo Herbelin
2018-05-23
*
Always print explanation for univ inconsistency, rm Flags.univ_print
Gaëtan Gilbert
2018-04-26
*
Fix #6956: Uncaught exception in bytecode compilation
Maxime Dénès
2018-04-06
*
Cumulativity: improve treatment of irrelevant universes.
Gaëtan Gilbert
2018-03-09
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
Adding a sanity check on inductive variance subtyping.
Pierre-Marie Pédrot
2018-02-15
*
Merge PR #6713: Fix #6677: Critical bug with VM and universes
Maxime Dénès
2018-02-14
|
\
|
*
Fix #6677: Critical bug with VM and universes
Maxime Dénès
2018-02-12
*
|
Universe instance printer: add optional variance argument.
Gaëtan Gilbert
2018-02-11
*
|
Simplification: cumulativity information is variance information.
Gaëtan Gilbert
2018-02-10
*
|
Fix typo in Univ.CumulativityInfo
Gaëtan Gilbert
2018-02-10
|
/
*
Moving some universe substitution code out of the kernel.
Pierre-Marie Pédrot
2017-12-30
*
Returning instance instead of substitution in universe context abstraction.
Pierre-Marie Pédrot
2017-12-30
*
Proper nametab handling of global universe names
Matthieu Sozeau
2017-12-01
*
When declaring constants/inductives use ContextSet if monomorphic.
Gaëtan Gilbert
2017-11-24
*
Use type nonrec in some functor arguments.
Gaëtan Gilbert
2017-10-16
*
Do not hashcons universes beforehand.
Pierre-Marie Pédrot
2017-09-01
*
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-27
*
The only abstraction-breaking function in Univ is now AUContext.instance.
Pierre-Marie Pédrot
2017-07-13
*
Cleaning up the implementation of module subtyping in the kernel.
Pierre-Marie Pédrot
2017-07-11
*
Less footguns in universe handling: remove subst_instance_context.
Pierre-Marie Pédrot
2017-07-11
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Clean up universes of constants and inductives
Amin Timany
2017-06-16
*
Simplify Univ.ml
Amin Timany
2017-06-16
*
Squashed commit of the following:
Amin Timany
2017-06-16
*
Check subtyping of inductive types in Kernel
Amin Timany
2017-06-16
*
Using UInfoInd for universes in inductive types
Amin Timany
2017-06-16
*
New datastructure for universes of inductive types
Amin Timany
2017-06-16
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
Remove some unused values and types
Gaetan Gilbert
2017-04-27
*
Document changes
Matthieu Sozeau
2016-12-02
*
Slightly more efficient [Univ.super] implem
Matthieu Sozeau
2016-11-30
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-30
|
\
|
*
A patch renaming equal into eq in the module dealing with
Hugo Herbelin
2016-03-22
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Universes algorithm : clarified comments
Jacques-Henri Jourdan
2016-01-17
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-29
|
\
|
|
*
Univs: entirely disallow instantiation of polymorphic constants with
Matthieu Sozeau
2015-11-27
|
*
Fix output of universe arcs. (Fix bug #4422)
Guillaume Melquiond
2015-11-23
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
|
\
|
|
*
Univs: update refman, better printers for universe contexts.
Matthieu Sozeau
2015-11-04
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
|
*
Adds support for the virtual machine to perform reduction of universe polymor...
Gregory Malecha
2015-10-28
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
|
\
|
|
*
Univs: fix bug #3807
Matthieu Sozeau
2015-10-08
*
|
Splitting kernel universe code in two modules.
Pierre-Marie Pédrot
2015-10-06
|
/
*
Univs: fix bug #4288, Print Sorted generated backward < constraints.
Matthieu Sozeau
2015-10-05
[next]