index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
checker
/
univ.ml
Age
Commit message (
Expand
)
Author
2016-07-03
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-03-22
A patch renaming equal into eq in the module dealing with
Hugo Herbelin
2016-01-20
Update copyright headers.
Maxime Dénès
2015-10-02
Univs: fix checker generating undeclared universes.
Matthieu Sozeau
2015-10-02
Univs: update checker
Matthieu Sozeau
2015-08-02
Reverting 16 last commits, committed mistakenly using the wrong push command.
Hugo Herbelin
2015-08-02
Hconsing continued
Hugo Herbelin
2015-02-11
Fixing bug #4019, and checker blow-up at once.
Pierre-Marie Pédrot
2015-02-11
Clarifying the implementation of universe hashconsing.
Pierre-Marie Pédrot
2015-01-12
Update headers.
Maxime Dénès
2015-01-06
Fix checker's treatment of template polymorphic
Matthieu Sozeau
2014-12-18
Backporting the change in lists of universes to the checker.
Pierre-Marie Pédrot
2014-12-17
checker: Change in library on disk values, now using context_sets instead of
Matthieu Sozeau
2014-12-17
Ensuring the good invariants of hashcons table generation in the API.
Pierre-Marie Pédrot
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
