index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
engine
/
uState.ml
Commit message (
Expand
)
Author
Age
*
[lib] Rename Profile to CProfile
Emilio Jesus Gallego Arias
2017-12-09
*
Merge PR #6290: Rename update to set, Fixes #6196
Maxime Dénès
2017-12-07
|
\
|
*
Rename update to set, fixes #6196
Paul Steckler
2017-12-05
*
|
Proper nametab handling of global universe names
Matthieu Sozeau
2017-12-01
|
/
*
Forbid repeated names in universe binders.
Gaëtan Gilbert
2017-11-25
*
Use Entries.constant_universes_entry more.
Gaëtan Gilbert
2017-11-24
*
restrict_universe_context: do not prune named universes.
Gaëtan Gilbert
2017-11-24
*
Separate checking univ_decls and obtaining universe binder names.
Gaëtan Gilbert
2017-11-24
*
Use Maps and ids for universe binders
Gaëtan Gilbert
2017-11-24
*
Use type Universes.universe_binders.
Gaëtan Gilbert
2017-11-24
*
Fix universe polymorphic Program obligations.
Matthieu Sozeau
2017-11-22
*
[api] Another large deprecation, `Nameops`
Emilio Jesus Gallego Arias
2017-11-13
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
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
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-07-04
|
\
*
|
Squashed commit of the following:
Amin Timany
2017-06-16
|
*
Univs: fix bug #5365, generation of u+k <= v constraints
Matthieu Sozeau
2017-06-05
*
|
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
*
|
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
\
|
*
|
Fast path when checking equality of universe levels in UState.
Pierre-Marie Pédrot
2017-04-27
|
*
|
Code cleaning in unification algorithm for universes.
Pierre-Marie Pédrot
2017-04-27
*
|
|
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
*
|
|
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-25
|
/
/
*
|
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
*
|
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-08-19
|
/
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Univ: Use loc even if there are more unbound levels
Matthieu Sozeau
2016-06-29
*
Univs: add source locations of levels
Matthieu Sozeau
2016-06-29
*
Allowing to attach location to universes in UState.
Pierre-Marie Pédrot
2016-02-19
*
Remove unneeded fixpoint in normalize_context_set. Note that it is no
Matthieu Sozeau
2015-12-01
*
More invariants in UState.
Pierre-Marie Pédrot
2015-11-26
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
*
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