index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
engine
/
universes.ml
Age
Commit message (
Expand
)
Author
2017-12-30
Moving some universe substitution code out of the kernel.
Pierre-Marie Pédrot
2017-12-09
[lib] Rename Profile to CProfile
Emilio Jesus Gallego Arias
2017-12-07
Merge PR #6290: Rename update to set, Fixes #6196
Maxime Dénès
2017-12-05
Rename update to set, fixes #6196
Paul Steckler
2017-12-01
Proper nametab handling of global universe names
Matthieu Sozeau
2017-11-25
Forbid repeated names in universe binders.
Gaëtan Gilbert
2017-11-25
Universe binders survive sections, modules and compilation.
Gaëtan Gilbert
2017-11-25
Allow local universe renaming in Print.
Gaëtan Gilbert
2017-11-24
Use Maps and ids for universe binders
Gaëtan Gilbert
2017-11-13
[api] Another large deprecation, `Nameops`
Emilio Jesus Gallego Arias
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-09-26
Merge PR #688: Binding universe constraints in Definition/Inductive/etc...
Maxime Dénès
2017-09-19
Allow declaring universe constraints at definition level.
Matthieu Sozeau
2017-09-08
Using EConstr equality check in unification.
Pierre-Marie Pédrot
2017-07-26
Removing template polymorphism for definitions.
Pierre-Marie Pédrot
2017-07-17
Merge PR #781: Remove dead code [Universes.simplify_universe_context]
Maxime Dénès
2017-07-13
Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.
Pierre-Marie Pédrot
2017-07-11
Less footguns in universe handling: remove subst_instance_context.
Pierre-Marie Pédrot
2017-07-11
Getting rid of simple calls to AUContext.instance.
Pierre-Marie Pédrot
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-20
Remove dead code [Universes.simplify_universe_context]
Gaëtan Gilbert
2017-06-16
Clean up universes of constants and inductives
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-02
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-04-27
Remove unused [open] statements
Gaetan Gilbert
2017-04-27
Add [_] prefix to unused values which maybe should be kept
Gaetan Gilbert
2017-03-24
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-21
[pp] Remove uses of expensive string_of_ppcmds.
Emilio Jesus Gallego Arias
2017-02-14
Evarconv API using EConstr.
Pierre-Marie Pédrot
2016-10-31
Stronger static invariant in equality upto universes.
Pierre-Marie Pédrot
2016-10-31
Code factorization in Universes.
Pierre-Marie Pédrot
2016-10-30
Moving Universes to the engine/ folder.
Pierre-Marie Pédrot
