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-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
[prev]
