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 Names in core.
Emilio Jesus Gallego Arias
2017-11-06
*
Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.
Maxime Dénès
2017-11-06
|
\
*
\
Merge PR #6072: Protecting evar map printer
Maxime Dénès
2017-11-06
|
\
\
*
\
\
Merge PR #6074: Refining PR#924 (insensitivity of projection heuristics to al...
Maxime Dénès
2017-11-06
|
\
\
\
*
\
\
\
Merge PR #6085: Update .mailmap with a jkloos alias
Maxime Dénès
2017-11-06
|
\
\
\
\
*
\
\
\
\
Merge PR #6063: Finish removing Show Goal uid
Maxime Dénès
2017-11-06
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6049: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" ...
Maxime Dénès
2017-11-06
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #1139: Add a linter.
Maxime Dénès
2017-11-06
|
\
\
\
\
\
\
\
|
|
|
|
*
|
|
|
Update .mailmap with a jkloos alias
Jason Gross
2017-11-05
|
|
_
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
Refining PR#924 (insensitivity of projection heuristics to alphabet).
Hugo Herbelin
2017-11-05
|
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
Cosmetic changes in evar_map printer.
Hugo Herbelin
2017-11-05
|
|
|
|
*
|
Preventively protect locally against failures of evar_map printer.
Hugo Herbelin
2017-11-05
|
|
|
|
*
|
Fixing a cause of failure of evar_map printer in debugger.
Hugo Herbelin
2017-11-05
|
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
*
[api] Deprecate all legacy uses of Name.Id in core.
Emilio Jesus Gallego Arias
2017-11-04
|
|
_
|
_
|
/
|
/
|
|
|
|
|
|
*
Finish removing Show Goal uid
Gaëtan Gilbert
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
|
|
|
|
|
|
|
|
|
|
|
*
provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules
Matej Košík
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
|
\
\
\
\
\
\
\
\
\
\
[next]
Emilio Jesus Gallego Arias
Maxime Dénès
Jason Gross
Hugo Herbelin
Gaëtan Gilbert
Farzon Lotfi
Matej Košík
Théo Zimmermann