index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2019-05-01
[comDefinition] Use prepare function from DeclareDef.
Emilio Jesus Gallego Arias
2019-05-01
Merge PR #10033: Remove the k0 argument from pretype functions.
Emilio Jesus Gallego Arias
2019-04-30
Merge PR #9947: Remove Global.env from goptions by passing from vernacentries
Emilio Jesus Gallego Arias
2019-04-30
Merge PR #10032: Remove leftover test suite file Quote.out
Emilio Jesus Gallego Arias
2019-04-30
Remove Global.env from goptions by passing from vernacentries
Gaëtan Gilbert
2019-04-30
Remove the k0 argument from pretype functions.
Jasper Hugunin
2019-04-30
Remove leftover test suite file Quote.out
Gaëtan Gilbert
2019-04-30
Merge PR #9939: Credits for 8.10
Vincent Laporte
2019-04-30
Change entry from #9651.
Théo Zimmermann
2019-04-30
Change entry for #10014.
Théo Zimmermann
2019-04-30
Add number of commits, PRs and issues closed.
Théo Zimmermann
2019-04-30
Advertize continuous deployment of documentation.
Théo Zimmermann
2019-04-30
More review suggestions.
Théo Zimmermann
2019-04-30
Remove remaining references to CHANGES.md from the Recent changes chapter.
Théo Zimmermann
2019-04-30
Remove misplaced CHANGES entry and fix links formatting.
Théo Zimmermann
2019-04-30
Finish adding authors and links to PRs.
Théo Zimmermann
2019-04-30
Change entry for #9906.
Théo Zimmermann
2019-04-30
Split changes between main changes and other changes (no repetition).
Théo Zimmermann
2019-04-30
Remove 8.10 entries from CHANGES file.
Théo Zimmermann
2019-04-30
First fixing pass, and experiment with dune-style PR number and author listing.
Théo Zimmermann
2019-04-30
Apply suggestions from code review
Théo Zimmermann
2019-04-30
Credits for 8.10
Matthieu Sozeau
2019-04-30
Merge PR #10019: Update behavior of -emacs to support showing diffs in ProofG...
Emilio Jesus Gallego Arias
2019-04-30
Merge PR #9995: fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType...
Enrico Tassi
2019-04-30
Merge PR #9952: Remove `constr_of_global_in_context`
Pierre-Marie Pédrot
2019-04-30
Merge PR #9349: Fix #9344, #9348: incorrect unsafe to_constr in vnorm
Maxime Dénès
2019-04-30
Merge PR #10024: [toplevel] Only print welcome header in standard coqtop.
Maxime Dénès
2019-04-30
fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType` interface
Georges Gonthier
2019-04-29
Merge PR #9983: Hypothesis conversion allocates a single evar
Hugo Herbelin
2019-04-29
Merge PR #9946: Add some entries to .mailmap
Emilio Jesus Gallego Arias
2019-04-29
Add some entries to .mailmap
Jason Gross
2019-04-29
Merge PR #9987: Fix #9180 by reverting #9249 and #8187
Emilio Jesus Gallego Arias
2019-04-29
Merge PR #9646: [proof] Fix proof bullet error helper which was implemented a...
Maxime Dénès
2019-04-29
Fix variant of #9344 for native_compute
Maxime Dénès
2019-04-29
[toplevel] Only print welcome header in standard coqtop.
Emilio Jesus Gallego Arias
2019-04-29
Fix #9344, #9348: incorrect unsafe to_constr in vnorm
Gaëtan Gilbert
2019-04-29
Merge PR #9651: [ssr] Add tactics under and over
Cyril Cohen
2019-04-29
Merge PR #9935: [api] [proof] Alert users that `Vernacstate.Proof_global` is ...
Maxime Dénès
2019-04-29
Merge PR #9775: inferCumulativity: shortcut for all-Invariant inductives
Pierre-Marie Pédrot
2019-04-29
Merge PR #9925: [vm] Protect accu and coq_env
Maxime Dénès
2019-04-29
Merge PR #10014: CoqIDE: load coqiderc after coqide.keys
Pierre-Marie Pédrot
2019-04-29
Merge PR #10007: Amending sphinx-on-windows fix in #9819 so that it does not ...
Vincent Laporte
2019-04-29
Merge PR #10011: [refman] Fix typo.
Vincent Laporte
2019-04-29
Merge PR #10018: Document unshelve (#3225)
Théo Zimmermann
2019-04-29
Merge PR #10021: More robust timing test.
Enrico Tassi
2019-04-29
Test-suite: add a case for issue #9180
Vincent Laporte
2019-04-29
Revert #8187
Vincent Laporte
2019-04-29
Revert #9249
Vincent Laporte
2019-04-29
More robust timing test.
Jason Gross
2019-04-29
Merge PR #9997: CoqIDE: fix open-file dialog and icons on macOS
Enrico Tassi
[next]