index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2018-11-14
ssr: add another test for elim + TC
Enrico Tassi
2018-11-14
ssr: rewrite: do resolve TC once and forall at the very end
Enrico Tassi
2018-11-14
ssr: elim: do resolve TC once and forall at the very end
Enrico Tassi
2018-11-14
ssrcommon: API to call resolve_tyclasses on a term
Enrico Tassi
2018-11-14
ssrmatching: unify_HO does not resolve type classes
Enrico Tassi
2018-11-14
[mailmap] Update "anonymous" accounts.
Théo Zimmermann
2018-11-14
Update .mailmap.
Théo Zimmermann
2018-11-14
Deprecate hint declaration/removal with no specified database
Maxime Dénès
2018-11-13
Merge PR #8886: [VM] Fix compilation of int31 eliminators
Maxime Dénès
2018-11-13
Merge PR #8906: [Goptions] More detailed error messages
Maxime Dénès
2018-11-13
Merge PR #8760: Automatically generate names for universes.
Pierre-Marie Pédrot
2018-11-13
coq_makefile: Fix ocamldep ignoring mlg files
Gaëtan Gilbert
2018-11-13
Merge PR #8976: CoqHammer CI
Gaëtan Gilbert
2018-11-13
Merge PR #8957: Fix -top for univbinders output test.
Emilio Jesus Gallego Arias
2018-11-13
Port to coqpp.
Pierre-Marie Pédrot
2018-11-13
Merge PR #8919: [vernac] Rename Vernacinterp to Vernacextend and move extensi...
Pierre-Marie Pédrot
2018-11-13
[vernac] Rename Vernacinterp to Vernacextend and move extension functions there.
Emilio Jesus Gallego Arias
2018-11-13
[configure] Remove grammar and dev from core_src_dirs.
Emilio Jesus Gallego Arias
2018-11-13
Merge PR #8978: nix helpers for debugging external projects from CI
Emilio Jesus Gallego Arias
2018-11-13
Merge PR #8936: Fix #8908: incorrect refresh of algebraic universes.
Pierre-Marie Pédrot
2018-11-12
Merge PR #8979: Skip submodules in HoTT CI script.
Emilio Jesus Gallego Arias
2018-11-12
Merge PR #8960: [dune] Build `cmxs` files instead of `cmxa` in "quick" target.
Enrico Tassi
2018-11-12
Skip submodules in HoTT CI script.
Gaëtan Gilbert
2018-11-12
Automatically generate names for universes.
Gaëtan Gilbert
2018-11-12
Do not qualify universe names by section path.
Gaëtan Gilbert
2018-11-12
Fix incorrect coq-prog-args in unidecls
Gaëtan Gilbert
2018-11-12
Don't declare universe binders for variables.
Gaëtan Gilbert
2018-11-12
Only declare univ binders once for mutind
Gaëtan Gilbert
2018-11-12
Merge PR #8962: [ci] Add paramcoq to CI.
Gaëtan Gilbert
2018-11-12
Merge PR #8892: Fix part of #8224: grounding open term in fixpoints
Pierre-Marie Pédrot
2018-11-12
Merge PR #8972: Fix #4771: Substitution of inline global reference in tactics...
Pierre-Marie Pédrot
2018-11-12
CoqHammer CI
Lukasz Czajka
2018-11-12
Set codeowners for dev/ci/nix
Vincent Laporte
2018-11-12
Helpers for debugging external projects from CI
Vincent Laporte
2018-11-12
Merge PR #8938: [Plugins] Remove some dead code
Pierre-Marie Pédrot
2018-11-12
Merge PR #8958: [clib] Remove unneeded `get_extension` function.
Pierre-Marie Pédrot
2018-11-12
Test case for #4771: Substitution of inline global reference in tactics is br...
Maxime Dénès
2018-11-12
Fix #4771: Substitution of inline global reference in tactics is broken
Maxime Dénès
2018-11-12
Fix #8908: incorrect refresh of algebraic universes.
Gaëtan Gilbert
2018-11-12
[clib] Remove unneeded `get_extension` function.
Emilio Jesus Gallego Arias
2018-11-11
CoqIDE: pass the parent window to all methods liable to open a question box.
Hugo Herbelin
2018-11-11
A private copy of lablgtk's question_box supporting the "parent" option.
Hugo Herbelin
2018-11-11
CoqIDE: ensure that the configuration box is not hidden by the main window.
Hugo Herbelin
2018-11-11
CoqIDE: remove obselete menu item "Complete word".
Hugo Herbelin
2018-11-11
CoqIDE: Do not rebind up and down in microPG mode.
Hugo Herbelin
2018-11-11
Merge PR #8795: Encapsulating declarations of primitive string syntax in a mo...
Jason Gross
2018-11-10
[ci] Add paramcoq to CI.
Emilio Jesus Gallego Arias
2018-11-09
Merge PR #8949: Remove checker printers
Emilio Jesus Gallego Arias
2018-11-09
Merge pull request #19 from SkySkimmer/gitignore
Emilio Jesús Gallego Arias
2018-11-09
Merge PR #8956: Fix dune runtest invocation
Emilio Jesus Gallego Arias
[prev]
[next]