index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
[api] Deprecate all legacy uses of Name.Id in core.
Emilio Jesus Gallego Arias
2017-11-04
*
Merge PR #6060: Improve error message and fix #6055 (spelling mistake).
Maxime Dénès
2017-11-03
|
\
*
\
Merge PR #6051: Fix FIXME: use OCaml 4.02 generative functors when available.
Maxime Dénès
2017-11-03
|
\
\
*
\
\
Merge PR #6047: A generic printer for ltac values
Maxime Dénès
2017-11-03
|
\
\
\
*
\
\
\
Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous varia...
Maxime Dénès
2017-11-03
|
\
\
\
\
*
\
\
\
\
Merge PR #6036: [toplevel] Export the last document seen after `Drop`.
Maxime Dénès
2017-11-03
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6031: [ci] Switch back to upstream version of Math-Classes and Corn.
Maxime Dénès
2017-11-03
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in dev/d...
Maxime Dénès
2017-11-03
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6024: Update of Coq version history
Maxime Dénès
2017-11-03
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition).
Maxime Dénès
2017-11-03
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #5999: An attempt to fix issue #5771 (error color hidden by warning ...
Maxime Dénès
2017-11-03
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge PR #924: Fixing part of #5669: unification heuristics sensitive to alph...
Maxime Dénès
2017-11-03
|
\
\
\
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
|
|
|
|
*
Update tactics.ml
Farzon Lotfi
2017-11-02
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
Ltac Debug: exporting env and sigma when needed so that term can be printed.
Hugo Herbelin
2017-11-02
|
|
|
|
|
|
|
|
|
*
|
Binding ltac printing functions to the system of generic printing.
Hugo Herbelin
2017-11-02
|
|
|
|
|
|
|
|
|
*
|
Setting a system to register printers for Ltac values.
Hugo Herbelin
2017-11-02
|
|
|
|
|
|
|
|
|
*
|
Exporting ValTMap for use in Genintern.
Hugo Herbelin
2017-11-02
|
|
|
|
|
|
|
|
|
*
|
Using a specific function to register vernac printers.
Hugo Herbelin
2017-11-02
|
|
|
|
|
|
|
|
|
*
|
Exporting the level-parametric printer of constr and its variants.
Hugo Herbelin
2017-11-02
|
|
|
|
|
|
|
|
|
*
|
Do not identify a pre_ident as a string Ltac value.
Hugo Herbelin
2017-11-02
|
|
|
|
|
|
|
|
|
*
|
Removing a redundancy in naming types (Ppconstr.precedence = tolerability).
Hugo Herbelin
2017-11-02
|
|
|
|
|
|
|
|
|
*
|
Naming the type of Dyn.Map for future reuse.
Hugo Herbelin
2017-11-02
|
|
|
|
|
|
|
|
|
*
|
Exporting a few more printing functions.
Hugo Herbelin
2017-11-02
|
|
|
|
|
|
|
|
|
*
|
Improving checks about the list separator in tactic notations.
Hugo Herbelin
2017-11-02
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
Fix FIXME: use OCaml 4.02 generative functors when available.
Gaëtan Gilbert
2017-11-01
|
|
|
*
|
|
|
|
|
|
Fixing #2881 ("change with" failing in an Ltac definition).
Hugo Herbelin
2017-10-30
|
|
|
|
|
_
|
_
|
_
|
_
|
/
|
|
|
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
*
Fixing #5401 (printing of patterns with bound anonymous variables).
Hugo Herbelin
2017-10-28
|
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
[toplevel] Export the last document seen after `Drop`.
Emilio Jesus Gallego Arias
2017-10-28
|
|
|
|
|
_
|
_
|
/
|
|
|
|
/
|
|
|
|
|
|
|
|
|
*
[ci] Switch back to upstream version of Math-Classes and Corn.
Théo Zimmermann
2017-10-27
|
|
|
|
|
_
|
/
|
|
|
|
/
|
|
|
|
|
|
|
*
Mention the migration from Bugzilla to GitHub issues in dev/doc/changes.
Théo Zimmermann
2017-10-27
|
|
|
|
|
/
|
|
|
|
/
|
*
|
|
|
|
Merge PR #6026: [ocaml] [travis] Add preliminary 4.06 CI testing.
Maxime Dénès
2017-10-27
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6015: [general] Remove Econstr dependency from `intf`
Maxime Dénès
2017-10-27
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631
Maxime Dénès
2017-10-27
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #5979: Fix #5763: Strictly positive example is out of order.
Maxime Dénès
2017-10-27
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #1113: Adding 3 Arith/QArith lemmas that I found useful
Maxime Dénès
2017-10-27
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #677: Trunk+abstracting injection flags
Maxime Dénès
2017-10-27
|
\
\
\
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
Chaining two tactics in a proof
Raphaël Monat
2017-10-27
|
|
|
|
|
|
*
|
|
|
[ocaml] [travis] Add preliminary 4.06 CI testing.
Emilio Jesus Gallego Arias
2017-10-27
|
|
_
|
_
|
_
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
Passing around the flag for injection so that tactics calling inj at
Hugo Herbelin
2017-10-26
|
*
|
|
|
|
|
|
|
Delay use of flag "Discriminate Introduction" from interp to execution time.
Hugo Herbelin
2017-10-26
|
|
|
|
|
|
|
|
*
Updating version history wrt 8.7.
Hugo Herbelin
2017-10-26
|
|
|
|
|
|
|
|
*
Updating version history wrt 8.6.
Hugo Herbelin
2017-10-26
|
|
|
|
|
|
|
|
*
Updating version history wrt 8.5.
Hugo Herbelin
2017-10-26
|
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
Rename \Tree to \NatTree
Johannes Kloos
2017-10-25
|
|
|
|
|
*
|
|
[general] Remove Econstr dependency from `intf`
Emilio Jesus Gallego Arias
2017-10-25
|
|
|
_
|
_
|
/
/
/
|
|
/
|
|
|
|
|
|
|
*
|
|
|
|
Moving from `is_true` to `= true`
Raphaël Monat
2017-10-25
*
|
|
|
|
|
|
Merge PR #6009: Master+misc typos dead code etc
Maxime Dénès
2017-10-25
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6003: Point HoTT back at master, which now supports Coq master
Maxime Dénès
2017-10-25
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #6002: Move bug files to match their new GitHub ID (fixes #6001).
Maxime Dénès
2017-10-25
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #5995: Revert "Add debug output to brew update."
Maxime Dénès
2017-10-25
|
\
\
\
\
\
\
\
\
\
\
[next]
Emilio Jesus Gallego Arias
Maxime Dénès
Farzon Lotfi
Hugo Herbelin
Gaëtan Gilbert
Théo Zimmermann
Raphaël Monat
Johannes Kloos