index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
vernac
/
obligations.ml
Commit message (
Expand
)
Author
Age
*
Allow using cumulativity without forcing strict constraints.
Gaëtan Gilbert
2018-03-09
*
Deprecate UState aliases in Evd.
Gaëtan Gilbert
2018-03-06
*
[econstr] Continue consolidation of EConstr API under `interp`.
Emilio Jesus Gallego Arias
2018-02-28
*
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2018-02-22
*
[flags] Make program_mode a parameter for commands in vernac.
Emilio Jesus Gallego Arias
2017-12-17
*
Merge PR #6275: [summary] Allow typed projections from global state.
Maxime Dénès
2017-12-12
|
\
|
*
[summary] Adapt STM to the new Summary API.
Emilio Jesus Gallego Arias
2017-12-09
*
|
Fix #6323: stronger restrict universe context vs abstract.
Gaëtan Gilbert
2017-12-06
|
/
*
Cleanup API for registering universe binders.
Matthieu Sozeau
2017-12-01
*
Merge PR #1033: Universe binder improvements
Maxime Dénès
2017-11-28
|
\
*
|
[api] Remove aliases of `Evar.t`
Emilio Jesus Gallego Arias
2017-11-26
|
*
Restrict universe context when declaring constants in obligations.
Gaëtan Gilbert
2017-11-25
|
*
Fix obligations handling of universes anticipating stronger restrict
Matthieu Sozeau
2017-11-25
|
*
Use Entries.constant_universes_entry more.
Gaëtan Gilbert
2017-11-24
|
*
When declaring constants/inductives use ContextSet if monomorphic.
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
|
/
*
Fix universe polymorphic Program obligations.
Matthieu Sozeau
2017-11-22
*
[api] Insert miscellaneous API deprecation back to core.
Emilio Jesus Gallego Arias
2017-11-13
*
[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
*
Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...
Maxime Dénès
2017-10-20
|
\
|
*
Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).
Hugo Herbelin
2017-10-05
*
|
[vernac] Remove `Qed exporting` syntax.
Emilio Jesus Gallego Arias
2017-09-29
|
/
*
Don't lose names in UState.universe_context.
Gaëtan Gilbert
2017-09-19
*
Allow declaring universe constraints at definition level.
Matthieu Sozeau
2017-09-19
*
Merge PR #841: Timorous fix of bug #5598 on global existing class in sections
Maxime Dénès
2017-08-16
|
\
*
|
Statically ensuring that inlined entries out of the kernel have no effects.
Pierre-Marie Pédrot
2017-07-26
*
|
More precise type for universe entries.
Pierre-Marie Pédrot
2017-07-26
*
|
Merge branch 'v8.7'
Maxime Dénès
2017-07-20
|
\
\
*
|
|
Removing the uses of abstraction-breaking code in Obligations.
Pierre-Marie Pédrot
2017-07-13
|
*
|
Deprecate options that were introduced for compatibility with 8.5.
Théo Zimmermann
2017-07-11
*
|
|
Safe API for accessing universe constraints of global references.
Pierre-Marie Pédrot
2017-07-11
|
/
/
|
*
Preparing to hints supporting discharge.
Hugo Herbelin
2017-06-27
|
/
*
[vernac] Remove forward hooks from Obligations.
Emilio Jesus Gallego Arias
2017-06-20
*
Clean up universes of constants and inductives
Amin Timany
2017-06-16
*
[proof] Deprecate redundant wrappers.
Emilio Jesus Gallego Arias
2017-06-11
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
Don't double up on periods in anomalies
Jason Gross
2017-06-02
*
Support for using type information to infer more precise evar sources.
Hugo Herbelin
2017-05-30
*
[coqlib] Deprecate redundant Coqlib functions.
Emilio Jesus Gallego Arias
2017-05-27
*
Merge PR#481: [option] Remove support for non-synchronous options.
Maxime Dénès
2017-05-25
|
\
*
\
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
\
|
|
*
[option] Remove support for non-synchronous options.
Emilio Jesus Gallego Arias
2017-05-24
|
|
/
|
*
Merge PR#627: Obligations shrinking: shrink abstraction too
Maxime Dénès
2017-05-20
|
|
\
|
*
|
Uniformity of style for selecting plural or not; spacing for comma.
Hugo Herbelin
2017-05-13
|
|
*
Obligations shrinking: shrink abstraction too
Matthieu Sozeau
2017-05-11
|
|
/
|
*
More consistent writing of de Bruijn.
Théo Zimmermann
2017-05-01
*
|
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
[next]