index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
engine
/
uState.mli
Commit message (
Expand
)
Author
Age
*
Document UState.universe_context.
Gaëtan Gilbert
2017-09-19
*
Don't lose names in UState.universe_context.
Gaëtan Gilbert
2017-09-19
*
proof_global: cleanup and comment close_proof
Matthieu Sozeau
2017-09-19
*
Allow declaring universe constraints at definition level.
Matthieu Sozeau
2017-09-19
*
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-27
*
Univs: fix bug #5365, generation of u+k <= v constraints
Matthieu Sozeau
2017-06-05
*
Adding a bit of documentation in the mli.
Pierre-Marie Pédrot
2016-06-09
*
Allowing to attach location to universes in UState.
Pierre-Marie Pédrot
2016-02-19
*
Fixing compilation of mli documentation.
Hugo Herbelin
2015-12-05
*
Remove unneeded fixpoint in normalize_context_set. Note that it is no
Matthieu Sozeau
2015-12-01
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-30
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
*
Clarifying and documenting the UState API.
Pierre-Marie Pédrot
2015-10-17
*
Dedicated file for universe unification context manipulation.
Pierre-Marie Pédrot
2015-10-17