index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2020-05-15
Moving interpretation of Search commands to their own file: comSearch.ml.
Hugo Herbelin
2020-05-15
Cleaning the use of pstate and evar_map in Search.
Hugo Herbelin
2020-05-15
Search: Displaying the "use About" notice only when really needed.
Hugo Herbelin
2020-05-15
Move SSR's Search to a new plugin and deprecate it.
Théo Zimmermann
2020-05-15
Addressing a suggestion from Théo Zimmermann.
Hugo Herbelin
2020-05-15
Search: new clauses for searching head, conclusion, kind...
Hugo Herbelin
2020-05-15
Renaming search_about_item into search_item.
Hugo Herbelin
2020-05-15
Update docgram following #12122 and #12229.
Théo Zimmermann
2020-05-15
Merge PR #12323: Fixes #12322: anomaly when printing "fun" binders with impli...
Emilio Jesus Gallego Arias
2020-05-15
Merge PR #11979: Add a rudimentary script to generate release changelog.
Emilio Jesus Gallego Arias
2020-05-15
Merge PR #11948: Hexadecimal numerals
Hugo Herbelin
2020-05-15
Merge PR #11755: [exn] [tactics] improve backtraces on monadic errors
Pierre-Marie Pédrot
2020-05-15
Merge PR #12243: Add a note on build-time dependencies to INSTALL.md.
Emilio Jesus Gallego Arias
2020-05-15
Merge PR #11992: do not re-export ListNotations from Program
Anton Trunov
2020-05-15
Merge PR #12032: [win] Elpi, Coq-Elpi and HB
Michael Soegtrop
2020-05-14
Merge PR #12256: Move the static check of evaluability in unfold tactic to ru...
Hugo Herbelin
2020-05-14
[exn] [tactics] improve backtraces on monadic errors
Emilio Jesus Gallego Arias
2020-05-14
Add advisories on OCaml setup to INSTALL.md.
Théo Zimmermann
2020-05-14
Merge PR #12296: Fixes #12234: wrong environment for Show Proof
Gaëtan Gilbert
2020-05-14
Merge PR #12327: Add a changelog for 8.11.2.
Théo Zimmermann
2020-05-14
Merge PR #11922: No more local reduction functions in Reductionops.
Maxime Dénès
2020-05-14
Add a changelog for 8.11.2.
Pierre-Marie Pédrot
2020-05-14
Merge PR #12312: Clarify the documentation for merging PRs with overlays
Théo Zimmermann
2020-05-14
Adding changelog.
Pierre-Marie Pédrot
2020-05-14
Remove an outdated piece of documentation about limitations of unfold.
Pierre-Marie Pédrot
2020-05-14
Tweak the error message of reference internalization.
Pierre-Marie Pédrot
2020-05-14
Add test for #11727, which was indirectly fixed by this PR.
Pierre-Marie Pédrot
2020-05-14
Generalize the interpretation of syntactic notation as reference to their head.
Pierre-Marie Pédrot
2020-05-14
Move the static check of evaluability in unfold tactic to runtime.
Pierre-Marie Pédrot
2020-05-14
Added change log.
Hugo Herbelin
2020-05-14
Fixes #12234 (wrong environment for Show Proof).
Hugo Herbelin
2020-05-14
Merge PR #12313: Make explicit that UGraph lower bounds are only of two kinds.
Gaëtan Gilbert
2020-05-14
Merge PR #12320: [ci] [sf] Fix SF build.
Gaëtan Gilbert
2020-05-14
Merge PR #12214: nit: don't open Persistent_cache in micromega
Vincent Laporte
2020-05-14
Add changelog for #12323.
Hugo Herbelin
2020-05-14
Fixes #12322 (anomaly when printing "fun" binders with implicit types).
Hugo Herbelin
2020-05-14
[ci] [sf] Fix SF build.
Emilio Jesus Gallego Arias
2020-05-14
Merge PR #12097: Interleave commandline require/set/unset commands
Emilio Jesus Gallego Arias
2020-05-14
Merge PR #8808: Extending support for mixing binders and terms in abbreviations
Emilio Jesus Gallego Arias
2020-05-14
Merge PR #12315: Tests for bugs #9583 (fixed by #11613) and #9679.
Emilio Jesus Gallego Arias
2020-05-14
Merge PR #12244: Store the OCaml version used for Coq in vo files.
Emilio Jesus Gallego Arias
2020-05-13
Adding change log for #8808.
Hugo Herbelin
2020-05-13
Overlay elpi
Hugo Herbelin
2020-05-13
Documenting notations with both terms and binders.
Hugo Herbelin
2020-05-13
Extending support for mixing binders and terms in abbreviations.
Hugo Herbelin
2020-05-13
Tests for bugs #9583 (fixed by #11613) and #9679.
Hugo Herbelin
2020-05-13
Merge PR #12293: Fix timestamp of coqchk manpage
Théo Zimmermann
2020-05-13
Make explicit that UGraph lower bounds are only of two kinds.
Pierre-Marie Pédrot
2020-05-13
do not re-export ListNotations from Program: kill overlays
Antonio Nikishaev
2020-05-13
Merge PR #12229: Hopefully consensual cleaning of keywords
Théo Zimmermann
[next]