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-19
[pfedit] Remove `start_proof` stub from `Pfedit`
Emilio Jesus Gallego Arias
2018-11-19
Merge PR #8987: Deprecate hint declaration/removal with no specified database
Pierre-Marie Pédrot
2018-11-19
Merge PR #9003: [vernacextend] Consolidate extension points API
Pierre-Marie Pédrot
2018-11-19
Merge PR #9026: [Documentation/Combined Scheme] Typo
Théo Zimmermann
2018-11-19
Typo: comment does not match code
Olivier Laurent
2018-11-19
Merge PR #8894: Print full binders in subtyping incompatible polymorphism error.
Pierre-Marie Pédrot
2018-11-19
Merge PR #8902: [ltac] Use CAst nodes in the tactic AST.
Pierre-Marie Pédrot
2018-11-19
Merge PR #9001: [options] Remove deprecated option automatic introduction.
Pierre-Marie Pédrot
2018-11-19
Merge PR #8999: [pfedit] Remove cook_proof stub.
Pierre-Marie Pédrot
2018-11-19
Merge PR #9023: [gramlib] Remove unused alias.
Pierre-Marie Pédrot
2018-11-19
Merge PR #9013: Do not Export the init modules
Pierre-Marie Pédrot
2018-11-19
Merge PR #8451: Print Universes Subgraph
Pierre-Marie Pédrot
2018-11-19
Merge PR #7881: Reimplement Store using Dyn
Pierre-Marie Pédrot
2018-11-19
[gramlib] Remove unused alias.
Emilio Jesus Gallego Arias
2018-11-18
[options] Remove deprecated option automatic introduction.
Emilio Jesus Gallego Arias
2018-11-18
Merge PR #9018: [devtools] Small script to setup overlays automatically
Gaëtan Gilbert
2018-11-17
Merge PR #8712: [stm] avoid unshare safe env to detect correctly env changing...
Maxime Dénès
2018-11-17
Merge PR #8992: put protocol/ in ide/.merlin
Pierre-Marie Pédrot
2018-11-17
Merge PR #8914: [CoqProject] Abstract warning function for CoqProject readers.
Pierre-Marie Pédrot
2018-11-17
[devtools] Small script to setup overlays automatically
Emilio Jesus Gallego Arias
2018-11-17
[vernacextend] Consolidate extension points API
Emilio Jesus Gallego Arias
2018-11-17
[ci] Uniformize casing of makefile targets and ci variables.
Emilio Jesus Gallego Arias
2018-11-17
[ci] Cleanup of old overlays.
Emilio Jesus Gallego Arias
2018-11-17
Merge PR #8968: Miscellaneous CoqIDE fixes
Pierre-Marie Pédrot
2018-11-17
[pfedit] Remove cook_proof stub.
Emilio Jesus Gallego Arias
2018-11-17
[CoqProject] Abstract warning function for CoqProject readers.
Emilio Jesus Gallego Arias
2018-11-17
[ltac] Use CAst nodes in the tactic AST.
Emilio Jesus Gallego Arias
2018-11-16
Merge PR #8779: Remove the implicit tactic feature following #7229.
Matthieu Sozeau
2018-11-16
Merge PR #8781: Remove primproj <-> constant dependency in Heads
Pierre-Marie Pédrot
2018-11-16
Reimplement Store using Dyn.
whitequark
2018-11-16
Add Dyn.anonymous, a more efficient version of Dyn.create (string_of_int n).
whitequark
2018-11-16
Use universe names when printing to dot.
Gaëtan Gilbert
2018-11-16
Print Universes Subgraph
Gaëtan Gilbert
2018-11-16
Make UGraph printing independent of hash order
Gaëtan Gilbert
2018-11-16
Print universe names in subtyping error instead of Var(x).
Gaëtan Gilbert
2018-11-16
We improve a little bit in printing universe constraints signature mismatch.
Hugo Herbelin
2018-11-16
Print full binders in subtyping incompatible polymorphism error.
Gaëtan Gilbert
2018-11-16
put protocol/ in ide/.merlin
Gaëtan Gilbert
2018-11-16
No Projection.constant in projection <-> constant declaration
Gaëtan Gilbert
2018-11-16
Heads: simplify using that projections are always rigid
Gaëtan Gilbert
2018-11-16
Do not Export the init modules
Gaëtan Gilbert
2018-11-16
Remove the implicit tactic feature following #7229.
Pierre-Marie Pédrot
2018-11-16
Merge PR #8888: Proof runcountable rebase
Hugo Herbelin
2018-11-15
Merge PR #8991: coqide: use correct toplevel name in files
Emilio Jesus Gallego Arias
2018-11-15
Move generating library dirpath to stm in compile mode.
Gaëtan Gilbert
2018-11-15
coqide: use correct toplevel name in files
Gaëtan Gilbert
2018-11-15
Make set_typing_flags "smart"
Gaëtan Gilbert
2018-11-15
Merge PR #8955: [ssr] "case/elim: p" don't resolve TC in "p"
Vincent Laporte
2018-11-14
Merge PR #8966: coq_makefile: Fix ocamldep ignoring mlg files
Emilio Jesus Gallego Arias
2018-11-14
ssr: add another test for elim + TC
Enrico Tassi
[next]