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
2021-01-20
Remove double induction tactic
Jim Fehrle
2021-01-19
Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)
Pierre-Marie Pédrot
2021-01-19
Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction pat...
Pierre-Marie Pédrot
2021-01-19
Merge PR #13725: Support locality attributes for Hint Rewrite (including export)
Pierre-Marie Pédrot
2021-01-18
Adding changelog for #13512.
Hugo Herbelin
2021-01-18
Support locality attributes for Hint Rewrite (including export)
Gaëtan Gilbert
2021-01-18
Merge PR #13574: Simplistic patch to fix #10113: turn Ltac2's `pattern:` into...
Pierre-Marie Pédrot
2021-01-18
Add changelog
Pierre Roux
2021-01-18
Merge PR #13705: Improve documentation of rewrite_strat/innermost and outermost
coqbot-app[bot]
2021-01-13
Adjust the doc_grammar files.
Théo Zimmermann
2021-01-07
Use nat_or_var for fail/gfail
Jim Fehrle
2021-01-07
Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... ...
Pierre-Marie Pédrot
2021-01-07
Merge PR #13715: [micromega] Add missing support for `implb`
Vincent Laporte
2021-01-06
Improve description of rewrite_strat/innermost and outermost
Jim Fehrle
2021-01-06
Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-m...
coqbot-app[bot]
2021-01-06
Merge PR #13714: Changelog for 8.13.0
coqbot-app[bot]
2021-01-06
[micromega] Add missing support for `implb`
BESSON Frederic
2021-01-05
[doc] tell sphinxcontrib-bibtex which bibtex file to use
Enrico Tassi
2021-01-04
Document the change of case representation.
Pierre-Marie Pédrot
2021-01-04
Changelog for 8.13.0
Enrico Tassi
2021-01-02
Deprecate "at ... with ..." in change tactic
Jim Fehrle
2021-01-01
Merge PR #13470: Convert rewriting and proof-mode chapters to prodn
coqbot-app[bot]
2020-12-30
Convert rewriting and proof-mode chapters to prodn
Jim Fehrle
2020-12-30
Merge PR #13684: Document the -native-compiler option
coqbot-app[bot]
2020-12-29
[refman] Clarify meaning of goal in documentation of instantiate.
Théo Zimmermann
2020-12-29
Document the -native-compiler option
Pierre Roux
2020-12-28
Merge PR #13665: Set Python's default output encoding to utf-8
coqbot-app[bot]
2020-12-26
Set the locale in Docker so Python's default output encoding is utf-8
Jim Fehrle
2020-12-21
Shorten/improve intro of "Basic proof writing" chapter.
Théo Zimmermann
2020-12-16
Merge PR #13643: Add -q flag to coqrst python invocation of coqtop
coqbot-app[bot]
2020-12-16
Add -q flag to coqrst python invocation of coqtop
Lasse Blaauwbroek
2020-12-16
Merge PR #13568: Fix #13566: Add checks for invalid occurrences in several ta...
Pierre-Marie Pédrot
2020-12-14
Adding change log for #13568.
Hugo Herbelin
2020-12-14
Merge PR #13613: [changes] mark #12765 as experimental
coqbot-app[bot]
2020-12-14
Merge PR #13509: Remove compatibility flag Set Bracketing Last Introduction P...
Pierre-Marie Pédrot
2020-12-13
Merge PR #13619: doc: Clarify the status of simpl vs cbn
coqbot-app[bot]
2020-12-13
Add changelog for #13509.
Hugo Herbelin
2020-12-13
Removing flag "Bracketing Last Introduction Pattern".
Hugo Herbelin
2020-12-11
doc: Clarify the status of simpl vs cbn
Clément Pit-Claudel
2020-12-11
Merge PR #13519: Better primitive type support in custom string and numeral n...
coqbot-app[bot]
2020-12-11
Merge PR #13611: Clarify changelog categories.
Clément Pit-Claudel
2020-12-11
Merge PR #13612: Bump reference to 8.12 refman following unexpected 8.12.2 re...
Clément Pit-Claudel
2020-12-11
Merge PR #13582: Generalize exp_ineq1 and add exp_ineq1_le, which holds foral...
coqbot-app[bot]
2020-12-11
[changes] mark #12765 as experimental
Enrico Tassi
2020-12-11
Bump reference to 8.12 refman following unexpected 8.12.2 release.
Théo Zimmermann
2020-12-11
Clarify changelog categories.
Théo Zimmermann
2020-12-10
Changelog for 8.12.2.
Théo Zimmermann
2020-12-09
Merge PR #13564: Allow all characters in tacn, cmd, ... names. Report duplic...
Clément Pit-Claudel
2020-12-09
Allow any character in a tacn, cmd, ... name
Jim Fehrle
2020-12-09
Redefines exp_ineq1 to hold for all non-zero numbers.
Avi Shinnar
[next]