index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
engine
Commit message (
Expand
)
Author
Age
*
Merge PR #6262: [error] Replace msg_error by a proper exception.
Maxime Dénès
2018-02-12
|
\
*
|
Simplification: cumulativity information is variance information.
Gaëtan Gilbert
2018-02-10
|
*
[error] Replace msg_error by a proper exception.
Emilio Jesus Gallego Arias
2018-02-09
|
/
*
Merge PR #6675: [proofview] enter_one: add __LOC__ argument to get relevant e...
Maxime Dénès
2018-02-01
|
\
|
*
Proofview: enter_one: add __LOC__ argument to get relevant error msg
Enrico Tassi
2018-01-31
*
|
Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.
Maxime Dénès
2018-01-31
|
\
\
*
\
\
Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.
Maxime Dénès
2018-01-22
|
\
\
\
|
|
_
|
/
|
/
|
|
|
*
|
Define EConstr version of [push_rec_types].
Cyprien Mangin
2018-01-19
*
|
|
Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.
Maxime Dénès
2018-01-18
|
\
\
\
|
|
/
/
|
/
|
|
*
|
|
Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)
Maxime Dénès
2018-01-17
|
\
\
\
|
|
*
|
Add a test that `prod_applist_assum` reduces the right number of let-ins
Jasper Hugunin
2018-01-17
|
|
*
|
Use let-in aware prod_applist_assum in dtauto and firstorder.
Jasper Hugunin
2018-01-17
|
|
/
/
|
/
|
|
|
|
*
Use a more efficient substitution composition in evar hypothesis naming.
Pierre-Marie Pédrot
2018-01-04
|
|
*
Cleanup name-binding structure for fresh evar name generation.
Pierre-Marie Pédrot
2018-01-02
*
|
|
Moving some universe substitution code out of the kernel.
Pierre-Marie Pédrot
2017-12-30
|
|
/
|
/
|
*
|
Merge PR #6222: Share computation of unifiable evars
Maxime Dénès
2017-12-22
|
\
\
*
\
\
Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.
Maxime Dénès
2017-12-18
|
\
\
\
*
\
\
\
Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`
Maxime Dénès
2017-12-15
|
\
\
\
\
*
\
\
\
\
Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.
Maxime Dénès
2017-12-14
|
\
\
\
\
\
|
|
|
*
|
|
[econstr] Add a couple of new API functions.
Emilio Jesus Gallego Arias
2017-12-13
|
|
|
/
/
/
|
|
*
/
/
[econstr] Cleanup in `vernac/classes.ml`.
Emilio Jesus Gallego Arias
2017-12-13
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Merge PR #6275: [summary] Allow typed projections from global state.
Maxime Dénès
2017-12-12
|
\
\
\
\
*
\
\
\
\
Merge PR #6368: [api] Remove yet another type alias.
Maxime Dénès
2017-12-11
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.
Maxime Dénès
2017-12-11
|
\
\
\
\
\
\
|
|
*
|
|
|
|
[api] Remove yet another type alias.
Emilio Jesus Gallego Arias
2017-12-09
|
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
[lib] Rename Profile to CProfile
Emilio Jesus Gallego Arias
2017-12-09
|
|
_
|
/
/
/
|
/
|
|
|
|
|
|
*
|
|
[summary] Adapt STM to the new Summary API.
Emilio Jesus Gallego Arias
2017-12-09
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Merge PR #6290: Rename update to set, Fixes #6196
Maxime Dénès
2017-12-07
|
\
\
\
\
|
|
*
|
|
Fix #6323: stronger restrict universe context vs abstract.
Gaëtan Gilbert
2017-12-06
|
|
/
/
/
|
/
|
|
|
|
*
|
|
Rename update to set, fixes #6196
Paul Steckler
2017-12-05
|
|
|
*
Fix #6297: handle constraints like (u+1 <= Set/Prop)
Gaëtan Gilbert
2017-12-01
|
|
|
/
|
|
/
|
*
|
|
Cleanup API for registering universe binders.
Matthieu Sozeau
2017-12-01
*
|
|
Proper nametab handling of global universe names
Matthieu Sozeau
2017-12-01
|
/
/
*
|
Merge PR #1033: Universe binder improvements
Maxime Dénès
2017-11-28
|
\
\
*
\
\
Merge PR #6248: [api] Remove aliases of `Evar.t`
Maxime Dénès
2017-11-28
|
\
\
\
|
*
|
|
[api] Remove aliases of `Evar.t`
Emilio Jesus Gallego Arias
2017-11-26
|
|
*
|
Forbid repeated names in universe binders.
Gaëtan Gilbert
2017-11-25
|
|
*
|
Universe binders survive sections, modules and compilation.
Gaëtan Gilbert
2017-11-25
|
|
*
|
Allow local universe renaming in Print.
Gaëtan Gilbert
2017-11-25
|
|
*
|
Make restrict_universe_context stronger.
Gaëtan Gilbert
2017-11-25
*
|
|
|
[lib] Generalize Control.timeout type.
Emilio Jesus Gallego Arias
2017-11-24
|
/
/
/
|
*
|
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
|
*
|
Stop exposing UState.universe_context and its Evd wrapper.
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
|
/
/
*
|
Merge PR #6203: Fix universe polymorphic Program obligations.
Maxime Dénès
2017-11-23
|
\
\
*
|
|
[api] A few more minor deprecation notices.
Emilio Jesus Gallego Arias
2017-11-22
*
|
|
[api] Deprecate Term destructors, move to Constr
Emilio Jesus Gallego Arias
2017-11-22
[next]
Maxime Dénès
Gaëtan Gilbert
Emilio Jesus Gallego Arias
Enrico Tassi
Cyprien Mangin
Jasper Hugunin
Pierre-Marie Pédrot
Paul Steckler
Matthieu Sozeau