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-12-21
Move lint job to gitlab
Gaëtan Gilbert
2018-12-21
Merge PR #9265: Do not exclude "opened" bugs from report
Gaëtan Gilbert
2018-12-21
Merge PR #9183: List members of the code of conduct enforcement team.
Matthieu Sozeau
2018-12-21
Do not exclude "opened" bugs from report
Maxime Dénès
2018-12-21
Merge PR #9182: Stop printing Monomorphic/Polymorphic in Print.
Maxime Dénès
2018-12-20
Merge PR #8488: Warning when using automatic template polymorphism
Pierre-Marie Pédrot
2018-12-20
Merge PR #9200: [ssr] make `>` stand alone
Maxime Dénès
2018-12-19
Add CHANGES for auto-template warning.
Gaëtan Gilbert
2018-12-19
Put #[universes(template)] in outputs tests
Gaëtan Gilbert
2018-12-19
Put #[universes(template)] on all auto template spots in stdlib
Gaëtan Gilbert
2018-12-19
warn when using auto template, funind never uses template poly
Gaëtan Gilbert
2018-12-19
Merge PR #9139: [engine] Allow debug printers to access the environment.
Pierre-Marie Pédrot
2018-12-19
Merge PR #9159: Make ugraph implementation abstract wrt universe specifics
Pierre-Marie Pédrot
2018-12-19
Merge PR #9231: Fixes #9229: Infix not robust wrt choice of variable names in...
Pierre-Marie Pédrot
2018-12-19
Merge PR #9237: Add Map.find_opt
Pierre-Marie Pédrot
2018-12-19
[doc] typo
Enrico Tassi
2018-12-19
Merge PR #9081: [dune] A new Makefile.dune target for each package (coq, coqi...
Théo Zimmermann
2018-12-19
[dune] Add targets for Coq individual packages.
Emilio Jesus Gallego Arias
2018-12-18
Merge PR #9223: Fix universe restriction in delayed mode.
Pierre-Marie Pédrot
2018-12-18
[ssr] make > a stand alone intro pattern
Enrico Tassi
2018-12-18
Merge PR #6705: [ssr] extended intro patterns
Cyril Cohen
2018-12-18
Fixes #9229 (Infix not robust wrt choice of variable names).
Hugo Herbelin
2018-12-18
[ssr] new test by Arthur Charguéraud
Enrico Tassi
2018-12-18
[ssr] extended intro patterns: + > [^] /ltac:
Enrico Tassi
2018-12-18
[arguments] cleanup
Enrico Tassi
2018-12-18
Merge PR #9218: [STM] Better protection for cur_id
Enrico Tassi
2018-12-18
Merge PR #9222: Fix classification of Set Default Proof Mode.
Enrico Tassi
2018-12-18
Add comment to acyclicgraph API
Gaëtan Gilbert
2018-12-18
Merge PR #9160: Avoid user-given names in automatic introduction of binders
Pierre-Marie Pédrot
2018-12-18
Merge PR #9178: CoqIDE: Restoring configuration of default width/height of ma...
Pierre-Marie Pédrot
2018-12-18
Merge PR #9215: Set up CI with Azure Pipelines
Emilio Jesus Gallego Arias
2018-12-17
Merge PR #9153: [api] Move reduction modules to `tactics`
Pierre-Marie Pédrot
2018-12-17
[STM] Better protection for cur_id
Maxime Dénès
2018-12-17
Merge PR #9238: CI: simple-io now depends on ext-lib
Emilio Jesus Gallego Arias
2018-12-17
Set up CI with Azure Pipelines
Gaëtan Gilbert
2018-12-17
simple-io now depends on ext-lib
Gaëtan Gilbert
2018-12-17
Merge PR #8856: [gitlab] Test Ocaml trunk.
Gaëtan Gilbert
2018-12-17
Restrict body universes in delayed mode.
Gaëtan Gilbert
2018-12-17
Fix git line ending conversion in windows
Gaëtan Gilbert
2018-12-17
Stop printing Monomorphic/Polymorphic in Print.
Gaëtan Gilbert
2018-12-17
Remove universe specific terminology from acyclicgraph
Gaëtan Gilbert
2018-12-17
Make ugraph implementation abstract wrt universe specifics
Gaëtan Gilbert
2018-12-17
Add Map.find_opt
Gaëtan Gilbert
2018-12-17
Fix classification of Set Default Proof Mode.
Gaëtan Gilbert
2018-12-17
Merge PR #9206: [stm] join the tip of the document even when fixing a proof (...
Emilio Jesus Gallego Arias
2018-12-17
Merge PR #9219: [STM] Fix logic of debug DAG printer
Enrico Tassi
2018-12-17
Merge PR #9220: Move shallow state logic to the function preparing state for ...
Enrico Tassi
2018-12-17
CoqIDE: Restoring configuration of default width/height of main window.
Hugo Herbelin
2018-12-16
Merge PR #9172: [proof] Rework proof interface.
Pierre-Marie Pédrot
2018-12-15
Avoid explicit names in binders for automatic intros
Jasper Hugunin
[next]