index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
Age
Commit message (
Expand
)
Author
2020-05-15
Move SSR's Search to a new plugin and deprecate it.
Théo Zimmermann
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 #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 #11992: do not re-export ListNotations from Program
Anton Trunov
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
Merge PR #12296: Fixes #12234: wrong environment for Show Proof
Gaëtan Gilbert
2020-05-14
Add a changelog for 8.11.2.
Pierre-Marie Pédrot
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
Added change log.
Hugo Herbelin
2020-05-14
Add changelog for #12323.
Hugo Herbelin
2020-05-14
Merge PR #12097: Interleave commandline require/set/unset commands
Emilio Jesus Gallego Arias
2020-05-13
Adding change log for #8808.
Hugo Herbelin
2020-05-13
Documenting notations with both terms and binders.
Hugo Herbelin
2020-05-13
Merge PR #12229: Hopefully consensual cleaning of keywords
Théo Zimmermann
2020-05-13
Merge PR #11828: [obligations] Deprecated flag cleanup
Gaëtan Gilbert
2020-05-13
Document the changes regarding the order of command-line options.
Théo Zimmermann
2020-05-12
Merge PR #12309: Remove documentation of -compile, which was removed in #8690.
Clément Pit-Claudel
2020-05-12
Merge PR #11503: Allow to rebind the old value of a mutable Ltac2 entry.
Jason Gross
2020-05-12
Merge PR #12223: Locating error again in atomic tactics (fixes #12152)
Pierre-Marie Pédrot
2020-05-12
Remove documentation of -compile, which was removed in #8690.
Théo Zimmermann
2020-05-12
Merge PR #12162: Fixing #12161: rename Bool.leb into Bool.le
Anton Trunov
2020-05-12
Merge PR #12146: Fixes #10812: tactic subst failure with section variables in...
Pierre-Marie Pédrot
2020-05-12
documenting with examples the dynamic behaviour of Ltac2 Set
Kenji Maillard
2020-05-12
fuse changelogs for #11249 and #12237
Olivier Laurent
2020-05-11
Merge PR #12254: In non-strict mode, accept any variable as a tactic reference.
Hugo Herbelin
2020-05-11
Correcting ltac2's documentation on values turning test into proper check.
Kenji Maillard
2020-05-11
Allow to rebind the old value of a mutable Ltac2 entry.
Pierre-Marie Pédrot
2020-05-11
Merge PR #12129: Add a `with_strategy` tactic
Pierre-Marie Pédrot
2020-05-10
Change log for #12223.
Hugo Herbelin
2020-05-10
Merge PR #12286: [sphinx] Add links to other versions of the refman
Théo Zimmermann
2020-05-09
[sphinx] Add links to other versions of the refman
Clément Pit-Claudel
2020-05-09
Merge PR #12241: [declare] Merge DeclareDef into Declare
Gaëtan Gilbert
2020-05-09
Revert "[with_strategy] Fix for coqchk"
Jason Gross
2020-05-09
[with_strategy] Work around #12191
Jason Gross
2020-05-09
Work around a bug in Coq in the doc
Jason Gross
2020-05-09
Elaborate with_strategy warning
Jason Gross
2020-05-09
Fix the `with_strategy` tactic to work with `abstract`
Jason Gross
2020-05-09
Add a `with_strategy` tactic
Jason Gross
2020-05-09
Hexadecimal: conversion to/from Coq strings
Pierre Roux
2020-05-09
Hexadecimal: proofs that conversions from/to nat,N,Z and Q are bijections
Pierre Roux
2020-05-09
[doc] Add hexadecimal numerals
Pierre Roux
2020-05-09
Decimal: specify numeral notation for Q
Pierre Roux
2020-05-09
Merge PR #12237: [stdlib] [List] add results around incl, filter and nth
Hugo Herbelin
2020-05-09
Merge PR #12163: Fix #12159 (Numeral Notations do not play well with multiple...
Hugo Herbelin
2020-05-08
Merge PR #12272: Cleanup formatting in .. coqtop:: directives
Clément Pit-Claudel
2020-05-09
Merge PR #12263: HaskellExtr: Add type annotations to Prelude.==
Kazuhiko Sakaguchi
[next]