index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
checker
/
univ.mli
Age
Commit message (
Expand
)
Author
2018-11-06
[checker] Refactor by sharing code with the kernel
Maxime Dénès
2018-06-21
Remove enforce_leq from checker
Gaëtan Gilbert
2018-05-13
Infrastructure for ocamldebug on the checker
Gaëtan Gilbert
2018-03-05
Replace invalid tag @raises in ocamldoc comments with @raise
mrmr1993
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-15
Adding a sanity check on inductive variance subtyping.
Pierre-Marie Pédrot
2018-02-10
Simplification: cumulativity information is variance information.
Gaëtan Gilbert
2017-12-30
Moving some universe substitution code out of the kernel.
Pierre-Marie Pédrot
2017-09-01
Do not hashcons universes beforehand.
Pierre-Marie Pédrot
2017-07-27
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-19
Fixing the checker w.r.t. wrongly used abstract universe contexts.
Pierre-Marie Pédrot
2017-07-11
Properly handling polymorphic inductive subtyping in the checker.
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-16
Clean up universes of constants and inductives
Amin Timany
2017-06-16
Enable the checking of ind subtyping in checker
Amin Timany
2017-06-16
Correct coqchk checking subtyping relation for inductives
Amin Timany
2017-06-16
Correct coqchk reduction
Amin Timany
2016-01-20
Update copyright headers.
Maxime Dénès
2016-01-06
Protect code against changes in Map interface.
Maxime Dénès
2015-10-02
Univs: fix checker generating undeclared universes.
Matthieu Sozeau
2015-10-02
Univs: update checker
Matthieu Sozeau
2015-01-12
Update headers.
Maxime Dénès
2015-01-06
Fix checker's treatment of template polymorphic
Matthieu Sozeau
2014-12-17
checker: Change in library on disk values, now using context_sets instead of
Matthieu Sozeau
2014-09-05
Remove unused substitution functions in checker.
Matthieu Sozeau
2014-09-05
Fix checker treatment of inductives using subst_instances instead of subst_un...
Matthieu Sozeau
2014-06-10
Removing dead code in checker/univ.ml.
Pierre-Marie Pédrot
2014-06-10
Removing explanations of universe inconsistencies from the checker. They
Pierre-Marie Pédrot
2014-06-10
Providing the checker with its own version of the Univ file.
Pierre-Marie Pédrot
