index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
Commit message (
Expand
)
Author
Age
*
Returning instance instead of substitution in universe context abstraction.
Pierre-Marie Pédrot
2017-12-30
*
Using a dedicated type for Lib.abstr_info.
Pierre-Marie Pédrot
2017-12-30
*
Merge PR #6469: No universe constraints in Let definitions
Maxime Dénès
2017-12-22
|
\
*
\
Merge PR #6449: Let definitions must not contain side-effects when reaching t...
Maxime Dénès
2017-12-20
|
\
\
|
|
*
Let definitions do not create new universe constraints.
Pierre-Marie Pédrot
2017-12-19
|
|
*
Specific type for section definition entries.
Pierre-Marie Pédrot
2017-12-19
|
|
/
*
|
Merge PR #6284: Warning for absolute name masking (deprecated, should become ...
Maxime Dénès
2017-12-18
|
\
\
|
|
*
Let definitions must not contain side-effects when reaching the kernel.
Pierre-Marie Pédrot
2017-12-16
|
|
/
|
/
|
*
|
Merge PR #6264: [kernel] Patch allowing to disable VM reduction.
Maxime Dénès
2017-12-14
|
\
\
*
\
\
Merge PR #6275: [summary] Allow typed projections from global state.
Maxime Dénès
2017-12-12
|
\
\
\
*
|
|
|
[api] Remove yet another type alias.
Emilio Jesus Gallego Arias
2017-12-09
|
*
|
|
[summary] Adapt STM to the new Summary API.
Emilio Jesus Gallego Arias
2017-12-09
|
*
|
|
[summary] Allow typed projections from global state + rework of internals.
Emilio Jesus Gallego Arias
2017-12-09
|
/
/
/
|
*
|
[kernel] Patch allowing to disable VM reduction.
Emilio Jesus Gallego Arias
2017-12-02
*
|
|
Proper nametab handling of global universe names
Matthieu Sozeau
2017-12-01
|
/
/
*
|
Merge PR #1049: Remove obsolete locality
Maxime Dénès
2017-11-30
|
\
\
|
|
*
Warning for absolute name masking (making it deprecated, should become
Matthieu Sozeau
2017-11-30
|
*
|
Remove "obsolete_locality" and fix STM vernac classification.
Maxime Dénès
2017-11-29
|
|
/
*
/
[lib] [api] Introduce record for `object_prefix`
Emilio Jesus Gallego Arias
2017-11-29
|
/
*
[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
*
[api] Miscellaneous consolidation + moves to engine.
Emilio Jesus Gallego Arias
2017-11-21
*
[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
*
Merge PR #6098: [api] Move structures deprecated in the API to the core.
Maxime Dénès
2017-11-13
|
\
*
\
Merge PR #6065: [api] Deprecate all legacy uses of Names in core.
Maxime Dénès
2017-11-13
|
\
\
*
|
|
[api] Remove 8.7 ML-deprecated functions.
Emilio Jesus Gallego Arias
2017-11-07
|
|
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
|
|
/
|
*
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-11-06
|
/
*
[api] Deprecate all legacy uses of Name.Id in core.
Emilio Jesus Gallego Arias
2017-11-04
*
Fix FIXME: use OCaml 4.02 generative functors when available.
Gaëtan Gilbert
2017-11-01
*
[stm] Remove state-handling from Futures.
Emilio Jesus Gallego Arias
2017-10-17
*
Merge PR #1114: Generic handling of nameable objects for plugins
Maxime Dénès
2017-10-09
|
\
*
|
[stm] [flags] Move document mode flags to the STM.
Emilio Jesus Gallego Arias
2017-10-06
|
*
Moving the Ltac-specific part of the nametab to the Ltac plugin.
Pierre-Marie Pédrot
2017-10-03
*
|
Removing now useless former fix to #3333 (check valid module names).
Hugo Herbelin
2017-09-12
|
/
*
Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name
Maxime Dénès
2017-08-31
|
\
*
\
Merge PR #773: [flags] Remove XML output flag.
Maxime Dénès
2017-08-29
|
\
\
|
|
*
Canonically renaming fold_map into fold_left_map in library Name.
Hugo Herbelin
2017-08-29
|
|
/
|
/
|
*
|
Print names of all open blocks
Tej Chajed
2017-08-06
|
*
[flags] Remove XML output flag.
Emilio Jesus Gallego Arias
2017-08-01
|
/
*
Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead
Maxime Dénès
2017-07-31
|
\
|
*
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-27
*
|
Removing template polymorphism for definitions.
Pierre-Marie Pédrot
2017-07-26
*
|
Remove a horrendous hack in Declare to retrieve exported side-effects.
Pierre-Marie Pédrot
2017-07-26
|
/
*
Merge PR #899: [general] Move files to directories so they match linking order.
Maxime Dénès
2017-07-20
|
\
*
|
Documenting the purity / marshallability invariant of persistent states.
Pierre-Marie Pédrot
2017-07-20
|
*
[general] Move files to directories matching linking order.
Emilio Jesus Gallego Arias
2017-07-19
|
/
*
Document the changes in API brought by this series of patches.
Pierre-Marie Pédrot
2017-07-14
*
Remove the function Global.type_of_global_unsafe.
Pierre-Marie Pédrot
2017-07-13
[next]