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
2019-04-29
Document unshelve (#3225)
Paolo G. Giarrusso
2019-04-28
Merge PR #9605: [coq_makefile] Enforce warn_error for plugins.
Gaëtan Gilbert
2019-04-27
Minor doc improvement.
Théo Zimmermann
2019-04-27
[refman] Fix typo.
Théo Zimmermann
2019-04-24
Merge PR #9988: [refman] Properly define token regexp.
Clément Pit-Claudel
2019-04-24
[refman] Fix a quoting problem.
Théo Zimmermann
2019-04-24
[refman] Properly define token regexp.
Théo Zimmermann
2019-04-24
[coq_makefile] Enforce warn_error for plugins.
Emilio Jesus Gallego Arias
2019-04-23
[ssr] under: optimization of the tactic for (under eq_bigl => *)
Erik Martin-Dorel
2019-04-23
[ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notations
Erik Martin-Dorel
2019-04-23
[doc] ssr_under: a few improvements
Enrico Tassi
2019-04-23
[ssr] under: Fix the defective form ("=> [*|*]" implied) and its doc
Erik Martin-Dorel
2019-04-23
[ssr] under: Fix and extend the documentation
Erik Martin-Dorel
2019-04-23
[ssr] new syntax for the under tactic
Enrico Tassi
2019-04-23
[ssr] under: Add doc for {under, over} & Add entry in CHANGES.md
Erik Martin-Dorel
2019-04-21
Remove duplicate copy of _warn_if_duplicate_name.
Jim Fehrle
2019-04-17
Merge PR #9876: Command-line setters for options
Emilio Jesus Gallego Arias
2019-04-16
Update and fix documentation of Program Fixpoint with measure
Maxime Dénès
2019-04-16
Command-line setters for options
Gaëtan Gilbert
2019-04-10
Improve SProp error message to mention the Allow StrictProp flag.
Théo Zimmermann
2019-04-05
Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)
Emilio Jesus Gallego Arias
2019-04-03
Merge PR #9078: Provide a faster bound name generation algorithm through a flag
Vincent Laporte
2019-04-03
Merge PR #9896: Minor correction to numeral notations doc
Théo Zimmermann
2019-04-03
Merge PR #8638: Remove -compat 8.7
Théo Zimmermann
2019-04-03
Minor correction to numeral notations doc
Jason Gross
2019-04-02
Merge PR #9668: Consolidate credits and changelog information in a single place.
Clément Pit-Claudel
2019-04-02
Remove -compat 8.7
Jason Gross
2019-04-02
Merge PR #9875: [doc] Add a note about Dune support to the manual.
Théo Zimmermann
2019-04-02
Document the Fast Name Printing option.
Pierre-Marie Pédrot
2019-04-02
Allow underscores as comments in numeral constants.
Pierre Roux
2019-04-02
Update documentation
Pierre Roux
2019-04-01
Merge PR #9725: Lia: various impovements (support for #8764, fix #9268 and ...
Vincent Laporte
2019-04-01
[doc] Add a note about Dune support to the manual.
Emilio Jesus Gallego Arias
2019-04-01
Update numeral notation printing doc
Jason Gross
2019-04-01
Several improvements and fixes of Lia
Frédéric Besson
2019-03-31
Move content of COMPATIBILITY to Changes chapter.
Théo Zimmermann
2019-03-31
Move V8 CHANGES to Changes chapter.
Théo Zimmermann
2019-03-31
Move V7 CHANGES to History chapter.
Théo Zimmermann
2019-03-31
Change main sections in history chapter.
Théo Zimmermann
2019-03-31
Split credits chapter in two parts: history, and changelog in inverse chronol...
Théo Zimmermann
2019-03-30
[Manual] Typo
Vincent Laporte
2019-03-29
typo in ring.rst
thery
2019-03-28
Merge PR #9129: [proof] Removal of imperative state ; interpretation layers o...
Maxime Dénès
2019-03-28
Merge PR #9743: Relax the ambiguous path condition of coercion
Enrico Tassi
2019-03-27
Merge PR #9828: Fix syntax of Typeclasses eauto := in reference manual.
Jim Fehrle
2019-03-27
[doc] [abstract] Document a bit some problems with abstract.
Emilio Jesus Gallego Arias
2019-03-27
[plugin tutorial] Adapt to removal of imperative state.
Emilio Jesus Gallego Arias
2019-03-27
Deprecate `Refine Instance Mode` option
Maxime Dénès
2019-03-26
Merge PR #9829: [Vernacular] Deprecate the “Show Script” command
Enrico Tassi
2019-03-26
Fix syntax of Typeclasses eauto := in reference manual.
Théo Zimmermann
[prev]
[next]