index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Also a less intrusive Profile.init_profile.
Hugo Herbelin
2017-07-20
*
A less intrusive Profile.close_profile.
Hugo Herbelin
2017-07-20
*
Merge PR #770: [proof] Move bullets to their own module.
Maxime Dénès
2017-07-19
|
\
*
\
Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag.
Maxime Dénès
2017-07-19
|
\
\
*
\
\
Merge PR #895: [ci] VST is now built with IGNORECOQVERSION=true.
Maxime Dénès
2017-07-19
|
\
\
\
|
*
|
|
[ci] VST is now built with IGNORECOQVERSION=true.
Théo Zimmermann
2017-07-18
|
/
/
/
*
|
|
Merge PR #781: Remove dead code [Universes.simplify_universe_context]
Maxime Dénès
2017-07-17
|
\
\
\
*
\
\
\
Merge PR #783: Remove some useless code in Term_typing
Maxime Dénès
2017-07-17
|
\
\
\
\
*
\
\
\
\
Merge PR #822: [meta] [api] Fix META file for API introduction.
Maxime Dénès
2017-07-17
|
\
\
\
\
\
|
|
|
|
*
|
[funind] Remove spurious character in comment.
Emilio Jesus Gallego Arias
2017-07-17
|
|
|
|
*
|
[API] Remove `open API` in ml files in favor of `-open API` flag.
Emilio Jesus Gallego Arias
2017-07-17
|
|
|
|
*
|
[meta] [api] Fix META file for API introduction.
Emilio Jesus Gallego Arias
2017-07-17
|
|
_
|
_
|
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers
Maxime Dénès
2017-07-17
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #881: Adapting base_include to 91df40272 (body_of_constant_body move...
Maxime Dénès
2017-07-17
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #879: Adding debug printers related to universes
Maxime Dénès
2017-07-17
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #874: Adding econstr printer to "include" file.
Maxime Dénès
2017-07-17
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #872: [travis] Display info on tested commit for PR builds.
Maxime Dénès
2017-07-17
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #865: RefMan-ext: fix some typos
Maxime Dénès
2017-07-17
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge PR #862: Adding support for bindings tags to explicit prefix/suffix rat...
Maxime Dénès
2017-07-17
|
\
\
\
\
\
\
\
\
\
\
\
|
|
|
|
|
|
*
|
|
|
|
|
Adapting to 91df40272 (body_of_constant_body moved to global).
Hugo Herbelin
2017-07-16
|
|
_
|
_
|
_
|
_
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
Update with non structurally recursive
william-lawvere
2017-07-14
|
|
|
|
|
*
|
|
|
|
|
Adding debug printers related to universes in the default debugger source file.
Pierre-Marie Pédrot
2017-07-14
|
|
_
|
_
|
_
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
Fix a typo in dev/changes.
Pierre-Marie Pédrot
2017-07-14
|
|
|
|
|
*
|
|
|
|
Document the changes in API brought by this series of patches.
Pierre-Marie Pédrot
2017-07-14
|
|
|
|
|
*
|
|
|
|
Getting rid of abstraction breaking code in tclABSTRACT.
Pierre-Marie Pédrot
2017-07-14
|
|
|
|
|
*
|
|
|
|
Removing a use of AUContext.instance in the STM.
Pierre-Marie Pédrot
2017-07-13
|
|
|
|
|
*
|
|
|
|
Removing the uses of abstraction-breaking code in Lemmas.
Pierre-Marie Pédrot
2017-07-13
|
|
|
|
|
*
|
|
|
|
Removing the uses of abstraction-breaking code in Obligations.
Pierre-Marie Pédrot
2017-07-13
|
|
|
|
|
*
|
|
|
|
Remove the function Global.type_of_global_unsafe.
Pierre-Marie Pédrot
2017-07-13
|
|
|
|
|
*
|
|
|
|
The only abstraction-breaking function in Univ is now AUContext.instance.
Pierre-Marie Pédrot
2017-07-13
|
|
|
|
|
*
|
|
|
|
Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.
Pierre-Marie Pédrot
2017-07-13
|
|
|
|
|
*
|
|
|
|
Getting rid of AUContext abstraction breakers in Elimschemes.
Pierre-Marie Pédrot
2017-07-13
|
|
|
|
|
*
|
|
|
|
Getting rid of AUContext abstraction breakers in Discharge.
Pierre-Marie Pédrot
2017-07-13
|
|
|
|
|
*
|
|
|
|
Make the typeclass implementation fully compatible with universe polymorphism.
Pierre-Marie Pédrot
2017-07-13
|
|
|
|
|
*
|
|
|
|
Safer API for Global.body_of_constant and variants.
Pierre-Marie Pédrot
2017-07-13
|
|
|
|
|
*
|
|
|
|
Safer API for Global.type_of_global_in_context.
Pierre-Marie Pédrot
2017-07-13
|
|
|
|
|
*
|
|
|
|
Getting rid of AUContext abstraction breakers in Record.
Pierre-Marie Pédrot
2017-07-13
|
|
|
|
|
*
|
|
|
|
Getting rid of AUContext abstraction breakers in Search.
Pierre-Marie Pédrot
2017-07-13
|
|
|
|
|
*
|
|
|
|
Getting rid of AUContext abstraction breakers in Recordops.
Pierre-Marie Pédrot
2017-07-13
|
|
_
|
_
|
_
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel
Maxime Dénès
2017-07-13
|
\
\
\
\
\
\
\
\
\
|
|
|
|
|
*
|
|
|
|
Adding econstr printer to "include" file.
Hugo Herbelin
2017-07-12
|
|
_
|
_
|
_
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
Adding a comment regarding De Bruijn universe indices in the kernel.
Pierre-Marie Pédrot
2017-07-12
|
|
|
|
*
|
|
|
|
[travis] Display info on tested commit for PR builds.
Théo Zimmermann
2017-07-11
*
|
|
|
|
|
|
|
|
Merge PR #871: Update Travis badge following the switch to master
Maxime Dénès
2017-07-11
|
\
\
\
\
\
\
\
\
\
|
*
|
|
|
|
|
|
|
|
Update Travis badge following the switch to master
Théo Zimmermann
2017-07-11
|
|
|
_
|
_
|
/
/
/
/
/
|
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
Moving the last bits of abtraction-breaking code out of the kernel.
Pierre-Marie Pédrot
2017-07-11
|
|
*
|
|
|
|
|
|
Fix nonsensical universe abstraction in the kernel.
Pierre-Marie Pédrot
2017-07-11
|
|
*
|
|
|
|
|
|
Properly handling polymorphic inductive subtyping in the checker.
Pierre-Marie Pédrot
2017-07-11
|
|
*
|
|
|
|
|
|
Properly handling polymorphic inductive subtyping in the kernel.
Pierre-Marie Pédrot
2017-07-11
|
|
*
|
|
|
|
|
|
Cleaning up the implementation of module subtyping in the kernel.
Pierre-Marie Pédrot
2017-07-11
[next]
Hugo Herbelin
Maxime Dénès
Théo Zimmermann
Emilio Jesus Gallego Arias
william-lawvere
Pierre-Marie Pédrot