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-03-26
Incorrect details in critical bug info (prop_set_proof_irrelevance)
Gaëtan Gilbert
2019-03-26
[kernel] Don't re-declare scheme side-effects that are already there.
Emilio Jesus Gallego Arias
2019-03-26
Fix make sphinx failure
Jim Fehrle
2019-03-26
Merge PR #9690: Fix 9663 (Miller pattern unification fails on evars)
Matthieu Sozeau
2019-03-26
Merge PR #9833: Improve the backport script.
Théo Zimmermann
2019-03-26
Merge PR #9489: [ssr] avoid HO unification to perform truncation analysy in elim
Maxime Dénès
2019-03-26
Ignore generated files for CoqIDE bindings
Vincent Laporte
2019-03-26
[evarconv] solve_simple_eqn is weaker than miller pattern (fix #9663)
Enrico Tassi
2019-03-26
Improve the backport script.
Guillaume Melquiond
2019-03-26
Merge PR #9826: [ssr] Two small improvements
Enrico Tassi
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
2019-03-26
Overlays for HoTT, Ltac2, and UniMath
Vincent Laporte
2019-03-26
Declare initial hint databases in prelude
Maxime Dénès
2019-03-26
Fix for https://github.com/coq/coq/pull/8984
Vincent Laporte
2019-03-25
Merge PR #8094: Remove `Automatic Coercions Import` option.
Pierre-Marie Pédrot
2019-03-25
[Vernacular] Deprecate the “Show Script” command
Vincent Laporte
2019-03-25
Move code ownership of reals library to new maintainer team.
Théo Zimmermann
2019-03-25
[ssr] Use Coqlib in “abstract”
Vincent Laporte
2019-03-25
[ssr] More detailed error message in rewrite
Vincent Laporte
2019-03-25
[ssr] avoid HO unif when doing truncation analysis
Enrico Tassi
2019-03-25
Remove `Automatic Coercions Import` option.
Maxime Dénès
2019-03-25
Merge PR #9823: Fix typo
Théo Zimmermann
2019-03-25
Merge PR #9586: Use named_context_val for fast lookup in intern named reference
Emilio Jesus Gallego Arias
2019-03-25
Fix #9652: rewrite fails to detect lack of progress
Gaëtan Gilbert
2019-03-25
Fix indentation
Gan Shen
2019-03-25
Update doc/sphinx/language/gallina-extensions.rst
Théo Zimmermann
2019-03-24
Fix typo
Gan Shen
2019-03-23
Merge PR #9822: [ci] [gitlab] Pin ocamlfind to master
Gaëtan Gilbert
2019-03-23
[ci] [gitlab] Pin ocamlfind to master
Emilio Jesus Gallego Arias
2019-03-22
Merge PR #8560: Unicode bindings for CoqIDE that works out of the box
Pierre-Marie Pédrot
2019-03-22
Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ...
Maxime Dénès
2019-03-21
Merge PR #9797: [ci] Fix OCaml trunk build.
Gaëtan Gilbert
2019-03-21
Merge PR #9789: [Manual] Improve documentation on Section, Variable, Context
Théo Zimmermann
2019-03-21
Merge PR #9695: [make install] Do not install the sphinx doctrees
Théo Zimmermann
2019-03-21
Merge PR #9774: Remove clutter by moving historic unmaintained dev/doc files ...
Emilio Jesus Gallego Arias
2019-03-20
[coq] Adapt to coq/coq#9129 "removal of imperative proof state"
Emilio Jesus Gallego Arias
2019-03-20
Merge pull request coq/ltac2#113 from maximedenes/printed-by-env
Pierre-Marie Pédrot
2019-03-20
Merge PR #9678: Stop accessing proof env via Pfedit in printers
Pierre-Marie Pédrot
2019-03-20
Merge PR #9776: [kernel] Fix compare_head_gen_leq_with to use [leq] on applic...
Gaëtan Gilbert
2019-03-20
Fix CoqIDE progress bar.
Pierre-Marie Pédrot
2019-03-20
Add overlays for printer API changes
Maxime Dénès
2019-03-20
Stop accessing proof env via Pfedit in printers
Maxime Dénès
2019-03-20
Merge PR #9791: Fix constr_matching on SProp
Pierre-Marie Pédrot
2019-03-20
Merge PR #8669: Show diffs in some error messages
Emilio Jesus Gallego Arias
2019-03-20
Merge PR #9746: Remove Term_typing.translate_mind indirection
Emilio Jesus Gallego Arias
2019-03-20
Merge PR #9770: Correct dependencies in the micromega pack
Emilio Jesus Gallego Arias
2019-03-20
Merge PR #9754: Don't lose the warning name when warning becomes error.
Emilio Jesus Gallego Arias
2019-03-20
Merge PR #9805: [CI] Push the right commit to cachix
Emilio Jesus Gallego Arias
2019-03-19
[CI] Push the right commit to cachix
Vincent Laporte
[prev]
[next]