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
*
Reuse the typing_flags datatype for inductives.
Pierre-Marie Pédrot
2016-06-18
*
Moving the typing_flags to the environment.
Pierre-Marie Pédrot
2016-06-18
*
Adding a local type-in-type flag in kernel declarations.
Pierre-Marie Pédrot
2016-06-18
*
Factorizing the uses of Declareops.safe_flags.
Pierre-Marie Pédrot
2016-06-16
*
Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.
Pierre-Marie Pédrot
2016-06-16
|
\
|
*
Assume totality: dedicated type rather than bool
Arnaud Spiwack
2016-06-14
*
|
Merge remote-tracking branch 'origin/pr/166' into trunk
Enrico Tassi
2016-06-14
|
\
\
*
\
\
Merge branch "LtacProf for trunk" (PR #165).
Pierre-Marie Pédrot
2016-06-14
|
\
\
\
*
|
|
|
Univs: more robust Universe/Constraint decls #4816
Matthieu Sozeau
2016-06-13
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-09
|
\
\
\
\
|
|
*
|
|
LtacProf for Coq trunk
Jason Gross
2016-06-05
|
|
/
/
/
|
/
|
|
|
|
*
|
|
Fix incorrect checking of library checksums.
Maxime Dénès
2016-06-05
*
|
|
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
|
|
*
|
coqc: support -o option to specify output file name
Enrico Tassi
2016-05-19
|
|
/
/
|
/
|
|
*
|
|
Dyn: simplify API introducing an Easy submodule
Enrico Tassi
2016-05-13
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-09
|
\
|
|
|
*
|
Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of Module.
Pierre-Marie Pédrot
2016-05-08
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-04
|
\
|
|
|
*
|
Fix bug #4292: Unexpected functor objects.
Pierre-Marie Pédrot
2016-05-03
*
|
|
Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into aspi...
Matthieu Sozeau
2016-04-04
|
\
\
\
*
\
\
\
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-05
|
\
\
\
\
|
|
|
/
/
|
|
/
|
|
|
*
|
|
Fix #4607: do not read native code files if native compiler was disabled.
Maxime Dénès
2016-03-04
*
|
|
|
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
\
\
\
\
*
\
\
\
\
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-02-13
|
\
\
\
\
\
|
|
|
/
/
/
|
|
/
|
|
|
|
|
*
|
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
|
|
/
/
/
|
/
|
|
|
|
*
|
|
Optimizing the universes_of_constr_function.
Pierre-Marie Pédrot
2016-02-03
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-29
|
\
|
|
|
|
*
|
|
Fix bug #4503: mixing universe polymorphic and monomorphic
Matthieu Sozeau
2016-01-23
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
|
|
*
|
|
Update copyright headers.
Maxime Dénès
2016-01-20
|
*
|
|
Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.
Maxime Dénès
2016-01-15
*
|
|
|
Changing "P is assumed" to "P is declared".
Hugo Herbelin
2016-01-14
*
|
|
|
merge
Matej Kosik
2016-01-11
|
\
\
\
\
|
*
|
|
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
|
|
|
Merge remote-tracking branch 'origin/v8.5' into trunk
Guillaume Melquiond
2016-01-06
|
\
\
\
\
\
|
|
|
/
/
/
|
|
/
|
|
|
|
*
|
|
|
Protect code against changes in Map interface.
Maxime Dénès
2016-01-06
*
|
|
|
|
Remove some unused functions.
Guillaume Melquiond
2016-01-02
*
|
|
|
|
Remove keys for evar and meta, since they cannot occur.
Guillaume Melquiond
2016-01-02
*
|
|
|
|
Remove some useless type declarations.
Guillaume Melquiond
2016-01-02
*
|
|
|
|
Remove Library.mem, which is pointless since 8.5.
Guillaume Melquiond
2015-12-31
*
|
|
|
|
Avoid a pointless conversion/copy.
Guillaume Melquiond
2015-12-22
*
|
|
|
|
Do not compose "str" and "to_string" whenever possible.
Guillaume Melquiond
2015-12-22
*
|
|
|
|
Move the From logic to Loadpath.expand_path.
Guillaume Melquiond
2015-12-22
*
|
|
|
|
Do not query module files that have already been loaded.
Guillaume Melquiond
2015-12-22
|
|
/
/
/
|
/
|
|
|
*
|
|
|
COMMENTS: added to some variants of "Globalnames.global_reference" type.
Matej Kosik
2015-12-18
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-08
|
\
|
|
|
*
|
|
|
Leveraging GADTs to provide a better Dyn API.
Pierre-Marie Pédrot
2015-12-05
*
|
|
|
Specializing the Dyn module to each usecase.
Pierre-Marie Pédrot
2015-12-04
|
*
|
|
Univs: fix bug #4443.
Matthieu Sozeau
2015-12-03
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-29
|
\
|
|
|
[next]
Pierre-Marie Pédrot
Arnaud Spiwack
Enrico Tassi
Matthieu Sozeau
Jason Gross
Maxime Dénès
Emilio Jesus Gallego Arias
Matej Kosik
Matthieu Sozeau
Hugo Herbelin
Guillaume Melquiond