index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
library
Age
Commit message (
Expand
)
Author
2018-09-20
Rewrite "Flags, Options and Tables" section.
Jim Fehrle
2018-09-19
Merge PR #8447: Cleaning in the retroknowledge
Pierre-Marie Pédrot
2018-09-18
Removing Dischargedhypsmap which is unused internally.
Maxime Dénès
2018-09-14
Retroknowledge: use GlobRef.t instead of Constr.t as entry
Vincent Laporte
2018-09-14
Retroknowledge: remove the (unused) by clause
Vincent Laporte
2018-09-12
Move maps & sets indexed by GlobRef.t into the kernel
Vincent Laporte
2018-09-05
[build] Preliminary support for building Coq with `dune`.
Emilio Jesus Gallego Arias
2018-09-03
Merge PR #7085: Turn the kernel reduction sharing flag into an argument passe...
Maxime Dénès
2018-07-27
Merge PR #8164: Add information to option type errors
Enrico Tassi
2018-07-26
Merge PR #8101: Remove ClosedModule and ClosedSection from libstack
Enrico Tassi
2018-07-26
Add information to option type errors
Tej Chajed
2018-07-26
Turn the kernel reduction sharing flag into an argument passed in the cache.
Pierre-Marie Pédrot
2018-07-24
Projections use index representation
Gaëtan Gilbert
2018-07-24
Move Heads to pretyping (is_projection will move to Recordops)
Gaëtan Gilbert
2018-07-20
Also remove ClosedSection (same reasoning as ClosedModule)
Maxime Dénès
2018-07-20
Remove ClosedModule from libstack
Maxime Dénès
2018-07-03
Library: use ocaml typing to show that we find at most 2 files
Gaëtan Gilbert
2018-07-03
Library.register_loaded_library: remove unused variable
Gaëtan Gilbert
2018-07-03
Libobject.apply_dyn_fun: remove unused deflt argument
Gaëtan Gilbert
2018-06-27
Swapping Context and Constr: defining declarations on constr in Constr.
Hugo Herbelin
2018-06-19
Merge PR #7797: Remove reference name type.
Enrico Tassi
2018-06-18
Remove reference name type.
Maxime Dénès
2018-06-17
Getting rid of the const_proj field in the kernel.
Pierre-Marie Pédrot
2018-06-14
Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ...
Pierre-Marie Pédrot
2018-06-12
[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-01
Merge PR #7234: Reduce circular dependency constants <-> projections
Maxime Dénès
2018-05-31
[api] Move `Constrexpr` to the `interp` module.
Emilio Jesus Gallego Arias
2018-05-31
Reduce circular dependency constants <-> projections
Gaëtan Gilbert
2018-05-30
[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-23
Collecting List.smart_* functions into a module List.Smart.
Hugo Herbelin
2018-05-18
Merge PR #6965: [api] Move universe syntax to `Glob_term`
Pierre-Marie Pédrot
2018-05-11
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-08
[api] Move universe syntax to `Glob_term`
Emilio Jesus Gallego Arias
2018-05-04
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-04-24
Don't recurse into closed modules/sections in split_lib.
Jasper Hugunin
2018-04-24
Remove DirClosedSection.
Jasper Hugunin
2018-04-23
[api] Relocate `intf` modules according to dependency-order.
Emilio Jesus Gallego Arias
2018-04-07
Fixes #7192 (Print Assumptions does not enter implementation of submodules).
Hugo Herbelin
2018-04-06
[api] Remove dependency of library on Vernacexpr.
Emilio Jesus Gallego Arias
2018-03-09
[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
[next]