index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2018-05-25
Merge PR #7598: Fix recipe for FAKEIDEBYTE
Enrico Tassi
2018-05-24
[tactics] Remove anonymous fix/cofix form.
Emilio Jesus Gallego Arias
2018-05-24
Fix recipe for FAKEIDEBYTE
Gaëtan Gilbert
2018-05-24
Adapt to fix/cofix changes in Coq (coq/coq#7196)
Emilio Jesus Gallego Arias
2018-05-24
Merge PR #7574: Improve merging and overlay documentations.
Emilio Jesus Gallego Arias
2018-05-24
Remove the unused printer_pr mechanism.
Jim Fehrle
2018-05-24
Complete rewrite of the documentation of overlays after Jim's additional comm...
Théo Zimmermann
2018-05-24
Relax advice on the name of user-overlays following Gaëtan's suggestion.
Théo Zimmermann
2018-05-24
Improve merging and overlay documentations.
Théo Zimmermann
2018-05-24
Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...
Pierre-Marie Pédrot
2018-05-24
Merge PR #7594: Fix #5983 (many frequent AppVeyor failures) by increasing spa...
Emilio Jesus Gallego Arias
2018-05-24
Fix #7323: coqchk puts polymorphic univs of inductive in global env
Gaëtan Gilbert
2018-05-24
[ide] Move common protocol library to its own folder/object.
Emilio Jesus Gallego Arias
2018-05-24
Merge PR #7581: Mention warning and error message docs in PR template
Théo Zimmermann
2018-05-24
Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constants
Pierre-Marie Pédrot
2018-05-24
Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant inst...
Pierre-Marie Pédrot
2018-05-24
Merge PR #7575: [build] Add -cclib -lcoqrun options to build of kernel.cmxa.
Enrico Tassi
2018-05-24
Fix #5983 (many frequent AppVeyor failures) by increasing spawn timeout.
Théo Zimmermann
2018-05-24
Merge PR #7582: [ci] Build fiat-crypto targets in sequence
Emilio Jesus Gallego Arias
2018-05-23
Don't try to install native compiled files if native-compile is not set
Jim Fehrle
2018-05-24
Merge PR #6515: [api] Move `Vernacexpr` to parsing.
Pierre-Marie Pédrot
2018-05-23
Fix #7586: Anomaly "Uncaught exception Not_found".
Pierre-Marie Pédrot
2018-05-23
Document Smart/Array changes in dev/doc/Changes.md.
Hugo Herbelin
2018-05-23
Renaming miscellaneous internal smart functions.
Hugo Herbelin
2018-05-23
Collecting Map.smart_* functions into a module Map.Smart.
Hugo Herbelin
2018-05-23
Moving Rtree.smart_map into Rtree.Smart.map.
Hugo Herbelin
2018-05-23
Moving Option.smart_map to Option.Smart.map.
Hugo Herbelin
2018-05-23
Collecting List.smart_* functions into a module List.Smart.
Hugo Herbelin
2018-05-23
Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.
Hugo Herbelin
2018-05-23
Collecting Array.smart_* functions into a module Array.Smart.
Hugo Herbelin
2018-05-23
Emphasizing the "smart"ness of Array.smartfoldmap{,2} in their documentation.
Hugo Herbelin
2018-05-23
CArray: adding combinators.
Hugo Herbelin
2018-05-23
Fix #7576: broken link for Delahaye paper.
Théo Zimmermann
2018-05-23
Remove unused references from biblio.
Théo Zimmermann
2018-05-23
Remove dashes from PR template
Jason Gross
2018-05-23
[api] Move `Vernacexpr` to parsing.
Emilio Jesus Gallego Arias
2018-05-23
[api] Move `opacity_flag` to `Proof_global`.
Emilio Jesus Gallego Arias
2018-05-23
Merge PR #7414: Add .byte targets for every bestocaml target
Enrico Tassi
2018-05-23
Merge PR #7567: Clean-up dead file in test-suite.
Enrico Tassi
2018-05-22
[ci] Build fiat-crypto targets in sequence
Jason Gross
2018-05-22
Merge PR #7565: Document the new nested-proof error message.
Emilio Jesus Gallego Arias
2018-05-22
Merge PR #7577: Fixing debugger after #6859 (loading dynlink.cma before lib.c...
Emilio Jesus Gallego Arias
2018-05-22
Mention warning and error message docs in PR template
Jason Gross
2018-05-22
Fixing debugger after #6859 (loading dynlink.cma before lib.cma).
Hugo Herbelin
2018-05-22
[doc] Document the new report_undocumented_coq_objects setting
Clément Pit-Claudel
2018-05-22
[doc] Add a list of common mistakes
Clément Pit-Claudel
2018-05-22
[doc] Fix an incorrect use of $PWD in Makefile.doc
Clément Pit-Claudel
2018-05-22
[doc] Add a setting to warn about empty Coq objects
Clément Pit-Claudel
2018-05-22
Merge PR #7384: Split Universes
Pierre-Marie Pédrot
2018-05-22
Add myself as a secondary maintainer for the documentation.
Théo Zimmermann
[prev]
[next]