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
*
Swapping Context and Constr: defining declarations on constr in Constr.
Hugo Herbelin
2018-06-27
*
Merge PR #7797: Remove reference name type.
Enrico Tassi
2018-06-19
|
\
|
*
Remove reference name type.
Maxime Dénès
2018-06-18
*
|
Getting rid of the const_proj field in the kernel.
Pierre-Marie Pédrot
2018-06-17
|
/
*
Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ...
Pierre-Marie Pédrot
2018-06-14
|
\
*
|
[api] Remove Misctypes.
Emilio Jesus Gallego Arias
2018-06-12
*
|
[api] Misctypes removal: several moves:
Emilio Jesus Gallego Arias
2018-06-12
*
|
[api] Misctypes removal: remove dummy alias.
Emilio Jesus Gallego Arias
2018-06-12
*
|
[api] Misctypes removal: miscellaneous aliases.
Emilio Jesus Gallego Arias
2018-06-12
*
|
[api] Misctypes removal: module_kind to Declaremods
Emilio Jesus Gallego Arias
2018-06-12
*
|
[api] Misctypes removal: multi to tactics/rewrite
Emilio Jesus Gallego Arias
2018-06-12
*
|
Merge PR #7234: Reduce circular dependency constants <-> projections
Maxime Dénès
2018-06-01
|
\
\
*
|
|
[api] Move `Constrexpr` to the `interp` module.
Emilio Jesus Gallego Arias
2018-05-31
|
*
|
Reduce circular dependency constants <-> projections
Gaëtan Gilbert
2018-05-31
*
|
|
[api] Remove deprecated objects in engine / interp / library
Emilio Jesus Gallego Arias
2018-05-30
*
|
|
[api] Remove deprecated object from `Term`
Emilio Jesus Gallego Arias
2018-05-30
|
/
/
*
|
Collecting List.smart_* functions into a module List.Smart.
Hugo Herbelin
2018-05-23
*
|
Merge PR #6965: [api] Move universe syntax to `Glob_term`
Pierre-Marie Pédrot
2018-05-18
|
\
\
*
\
\
Merge PR #7340: Remove DirClosedSection.
Enrico Tassi
2018-05-11
|
\
\
\
*
\
\
\
Merge PR #7341: Don't recurse into closed modules/sections in split_lib.
Enrico Tassi
2018-05-11
|
\
\
\
\
|
|
|
*
|
[api] Move universe syntax to `Glob_term`
Emilio Jesus Gallego Arias
2018-05-08
|
|
_
|
/
/
|
/
|
|
|
*
|
|
|
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-05-04
|
*
|
|
Don't recurse into closed modules/sections in split_lib.
Jasper Hugunin
2018-04-24
|
/
/
/
|
*
/
Remove DirClosedSection.
Jasper Hugunin
2018-04-24
|
/
/
*
|
[api] Relocate `intf` modules according to dependency-order.
Emilio Jesus Gallego Arias
2018-04-23
|
*
Fixes #7192 (Print Assumptions does not enter implementation of submodules).
Hugo Herbelin
2018-04-07
*
|
[api] Remove dependency of library on Vernacexpr.
Emilio Jesus Gallego Arias
2018-04-06
|
/
*
[located] Push inner locations in `reference` to a CAst.t node.
Emilio Jesus Gallego Arias
2018-03-09
*
Merge PR #6775: Allow using cumulativity without forcing strict constraints.
Maxime Dénès
2018-03-09
|
\
|
*
Allow using cumulativity without forcing strict constraints.
Gaëtan Gilbert
2018-03-09
*
|
Implement the Export Set/Unset feature.
Pierre-Marie Pédrot
2018-03-09
*
|
Export the various option localities in the API.
Pierre-Marie Pédrot
2018-03-09
|
/
*
Use a proper warning when a summary is captured out of module scope.
Vincent Laporte
2018-03-07
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2018-02-22
*
Extrude monomorphic universe contexts from with Definition constraints.
Pierre-Marie Pédrot
2018-02-16
*
Use r.(p) syntax to print primitive projections.
Maxime Dénès
2018-01-30
*
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
|
/
/
/
[next]