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-11
Generalize map_named_val to handle whole declarations.
Pierre-Marie Pédrot
2019-05-11
Abstract the Tactic.e_change_hyps function over the reduction function.
Pierre-Marie Pédrot
2019-05-11
Merge PR #10052: Cleanup the hypothesis conversion function
Hugo Herbelin
2019-05-10
Use Print Custom Grammar to inspect custom entries
Jasper Hugunin
2019-05-10
[refman] Mention the `#[canonical(false)]` attribute
Vincent Laporte
2019-05-10
[Attributes] Allow explicit value for two-valued attributes
Vincent Laporte
2019-05-10
Add overlay for elpi
Vincent Laporte
2019-05-10
Changelog for PR #10076
Vincent Laporte
2019-05-10
[User manual] Fix two warnings related to canonical structures
Vincent Laporte
2019-05-10
[Canonical structures] “not_canonical” annotation to field declarations
Vincent Laporte
2019-05-10
[Canonical structures] Some projections may not be canonical
Vincent Laporte
2019-05-10
Merge PR #10058: Remove various circumvolutions from reduction behaviors
Enrico Tassi
2019-05-10
Merge PR #10080: Define minimum Sphinx version in conf.py.
Clément Pit-Claudel
2019-05-10
[ltac2] Add primitive integers
Pierre Roux
2019-05-10
Merge PR #9854: Improve field_simplify on fractions with constant denominator
Michael Soegtrop
2019-05-10
Merge PR #10065: CI: run coqchk without -silent
Emilio Jesus Gallego Arias
2019-05-10
Add overlays for coq/coq#10052.
Pierre-Marie Pédrot
2019-05-10
Fast-path for reordering of a single closed variable.
Pierre-Marie Pédrot
2019-05-10
Take advantage of the ordering / conversion check split.
Pierre-Marie Pédrot
2019-05-10
Split the hypothesis conversion check in a conversion + ordering check.
Pierre-Marie Pédrot
2019-05-10
Make the check flag of conversion functions mandatory.
Pierre-Marie Pédrot
2019-05-10
Logic.convert_hyp now takes an environment as an argument.
Pierre-Marie Pédrot
2019-05-10
Cleanup of Logic.convert_hyp.
Pierre-Marie Pédrot
2019-05-10
Remove ref from some implicit_discharge_request
Jasper Hugunin
2019-05-10
Simplify dispose_implicits
Jasper Hugunin
2019-05-10
Remove various circumvolutions from reduction behaviors
Maxime Dénès
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-10
[api] Remove 8.10 deprecations.
Emilio Jesus Gallego Arias
2019-05-10
Better title for the first example of the Ltac examples section.
Théo Zimmermann
2019-05-09
Merge PR #10081: Remove ppedrot/ltac2 from CI after integration in main repo
Michael Soegtrop
2019-05-09
Switched Coquelicot CI URLs from INRIA gforge to INRIA gitlab
Michael Soegtrop
2019-05-09
Improve the first two Ltac examples.
Théo Zimmermann
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
Rewording, language improvements.
Théo Zimmermann
2019-05-09
Merge PR #10069: Do not use the constant stack in whd_betaiota_deltazeta_for_...
Hugo Herbelin
2019-05-08
[refman] Move all the Ltac examples to the Ltac chapter.
Théo Zimmermann
2019-05-08
Update release process documentation and changelog entry.
Théo Zimmermann
2019-05-08
Add a test that unreleased changelog of released versions is empty.
Théo Zimmermann
2019-05-08
Define a new `is_a_released_version` variable in configure.ml.
Théo Zimmermann
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
[prev]
[next]