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-10
Merge PR #10065: CI: run coqchk without -silent
Emilio Jesus Gallego Arias
2019-05-10
CI: run coqchk without -silent
Gaëtan Gilbert
2019-05-10
Merge PR #10120: Clean-up: remove dead appveyor.sh file.
Emilio Jesus Gallego Arias
2019-05-09
Merge PR #10081: Remove ppedrot/ltac2 from CI after integration in main repo
Michael Soegtrop
2019-05-09
Merge PR #10046: [primitive integers] Make div21 implems consistent with its ...
Maxime Dénès
2019-05-09
Merge PR #10126: Ignore generated dune file for Ltac2
Gaëtan Gilbert
2019-05-09
Ignore generated dune file for Ltac2
Vincent Laporte
2019-05-09
Merge PR #10082: Fix PLUGINSVO computation after ltac2 integration
Maxime Dénès
2019-05-09
Merge PR #10069: Do not use the constant stack in whd_betaiota_deltazeta_for_...
Hugo Herbelin
2019-05-08
Remove ltac2 add-on from Windows installer now that it is in the main Coq pac...
Théo Zimmermann
2019-05-08
Clean-up: remove dead appveyor.sh file.
Théo Zimmermann
2019-05-08
Merge PR #10087: Added description of Q
Théo Zimmermann
2019-05-08
Merge PR #10086: Fix gitignore for ltac2
Pierre-Marie Pédrot
2019-05-08
Merge PR #10119: Show diffs in error messages only if Diffs is enabled
Gaëtan Gilbert
2019-05-07
Show diffs in error messages only if Diffs is enabled
Jim Fehrle
2019-05-07
Added "Recursively" for the R option
Robert Rand
2019-05-07
Added description of Q
Robert Rand
2019-05-07
Fix gitignore for ltac2
Gaëtan Gilbert
2019-05-07
Merge PR #10077: [refman] Add a note reminding about the typeclass_instances ...
Clément Pit-Claudel
2019-05-07
Merge PR #10016: [test-suite] Remove a test with a Timeout that fails frequen...
Vincent Laporte
2019-05-07
Fix PLUGINSVO computation after ltac2 integration
Gaëtan Gilbert
2019-05-07
Remove ppedrot/ltac2 from CI after integration in main repo
Gaëtan Gilbert
2019-05-07
Merge PR #10053: Document change_no_check variants
Théo Zimmermann
2019-05-07
Merge PR #10075: [Record] Une a record to gather field declaration attributes
Enrico Tassi
2019-05-07
Merge PR #10002: Integrate ltac2
Théo Zimmermann
2019-05-07
[refman] Add a note reminding about the typeclass_instances database.
Théo Zimmermann
2019-05-07
Merge PR #10063: CoqIDE: recognize qualified identifiers as words.
Pierre-Marie Pédrot
2019-05-07
Add overlays.
Pierre-Marie Pédrot
2019-05-07
Do not use the constant stack in whd_betaiota_deltazeta_for_iota_state.
Pierre-Marie Pédrot
2019-05-07
[Record] Une a record to gather field declaration attributes
Vincent Laporte
2019-05-07
[Record] Deforestation
Vincent Laporte
2019-05-07
[Canonical structures] Deforestation
Vincent Laporte
2019-05-07
Integrate build and documentation of Ltac2
Maxime Dénès
2019-05-06
Merge PR #10068: Coqchk: encapsulating an anomaly NotConvertible into a prope...
Pierre-Marie Pédrot
2019-05-06
Merge PR #9964: Unreleased changelog folder
Vincent Laporte
2019-05-06
Coqchk: encapsulating an anomaly NotConvertible into a proper typing error.
Hugo Herbelin
2019-05-05
Add changelog entry about moving changelog to refman.
Théo Zimmermann
2019-05-05
[make] build unreleased.rst
Enrico Tassi
2019-05-05
Create categories in changelog.
Théo Zimmermann
2019-05-05
New infrastructure for the unreleased changelog.
Théo Zimmermann
2019-05-05
Merge PR #10059: Fixing bugs introduced in change_no_check
Pierre-Marie Pédrot
2019-05-04
Merge PR #9926: [vernac] [ast] Make location info an attribute of vernaculars.
Pierre-Marie Pédrot
2019-05-04
Merge PR #9996: Fix #5752: `Hint Mode` ignored for type classes that appear a...
Pierre-Marie Pédrot
2019-05-04
Merge PR #10012: Document convert_concl_no_check (#3225)
Théo Zimmermann
2019-05-04
Merge PR #10057: Fix #10054: Numeral Notations without the ltac plugin.
Emilio Jesus Gallego Arias
2019-05-03
CoqIDE: recognize qualified identifiers as words.
Jasper Hugunin
2019-05-03
Tactics: fixing "change_no_check in".
Hugo Herbelin
2019-05-03
Updating CHANGES.
Hugo Herbelin
2019-05-03
Merge PR #9984: Add PairUsualDecidableTypeFull
Théo Zimmermann
2019-05-03
Remove now useless commented code
Pierre Roux
[next]