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-07
Merge PR #8934: Revert "Do not allow spliting in res_pf, this is reserved for...
Matthieu Sozeau
2018-11-07
Merge PR #8928: Fixes #8910: typo in nameops.ml
Pierre-Marie Pédrot
2018-11-07
Merge PR #8901: [dune] Add "quick" and "check" targets for fast builds.
Gaëtan Gilbert
2018-11-07
Merge PR #8927: Optimise git cloning
Gaëtan Gilbert
2018-11-07
Revert "Do not allow spliting in res_pf, this is reserved for pretyping"
Enrico Tassi
2018-11-07
Merge PR #8918: Fix overlays on Windows CI
Michael Soegtrop
2018-11-07
Merge PR #8868: [Docker] Update OCaml (4.07.1) and camlp5 (7.07-almost)
Emilio Jesus Gallego Arias
2018-11-07
Merge PR #8773: [checker] Refactor by sharing code with the kernel
Pierre-Marie Pédrot
2018-11-07
Merge PR #8926: Move features that were not backported to 8.9 to the 8.10 sec...
Guillaume Melquiond
2018-11-06
Fixes #8910 (typo in nameops.ml).
Hugo Herbelin
2018-11-06
Optimise git cloning
Kamil Trzciński
2018-11-06
Move features that were not backported to 8.9 to the 8.10 section of CHANGES.md.
Théo Zimmermann
2018-11-06
Merge PR #8889: Program hook gives back an obligation substitiution
Pierre-Marie Pédrot
2018-11-06
[dune] Add "quick" and "check" targets for fast builds.
Emilio Jesus Gallego Arias
2018-11-06
[Docker] Update COMPILER_EDGE: 4.07.0 → 4.07.1
Vincent Laporte
2018-11-06
Fix overlays on Windows CI
Gaëtan Gilbert
2018-11-06
Bring back context printing in checker
Maxime Dénès
2018-11-06
Checker now disables VM and native
Maxime Dénès
2018-11-06
Remove checker files from .gitignore
Maxime Dénès
2018-11-06
[checker] Check univ constraints induced by module subtyping
Maxime Dénès
2018-11-06
[checker] Fix "error related to inductive types"
Maxime Dénès
2018-11-06
[checker] Refactor by sharing code with the kernel
Maxime Dénès
2018-11-06
Move debug term printer to kernel
Maxime Dénès
2018-11-06
Merge PR #8912: [dune] [coqide] Use copy action instead of (run cp ...)
Théo Zimmermann
2018-11-06
Merge PR #8903: [dune] Add to vo rules explicit location of coqlib in boot mode.
Théo Zimmermann
2018-11-06
Merge PR #8884: Improve rendering of the credits.
Théo Zimmermann
2018-11-06
Merge PR #8556: [ssr] use tclDISPATCH for IPatDispatch (fix #8544)
Maxime Dénès
2018-11-06
Merge PR #8915: More cleanup of vendored camlp5
Emilio Jesus Gallego Arias
2018-11-06
Removing dead code in Plexing.
Pierre-Marie Pédrot
2018-11-06
Remove the non-functorial interface of camlp5 grammars.
Pierre-Marie Pédrot
2018-11-06
Add overlay for Equations
Matthieu Sozeau
2018-11-06
[program] extend obligation to give back a mapping from obligations to
Matthieu Sozeau
2018-11-06
Improve rendering of the credits.
Guillaume Melquiond
2018-11-06
Merge PR #8907: Cleanup camlp5 dead code
Emilio Jesus Gallego Arias
2018-11-06
[dune] [coqide] Use copy action instead of (run cp ...)
Emilio Jesus Gallego Arias
2018-11-05
Remove patches of dead code in Gramlib.
Pierre-Marie Pédrot
2018-11-05
Remove the Scut constructor from Gramlib.
Pierre-Marie Pédrot
2018-11-05
Remove the Sflag constructor from Gramlib.
Pierre-Marie Pédrot
2018-11-05
Remove the Sfacto constructor from Gramlib.
Pierre-Marie Pédrot
2018-11-05
Remove the Svala constructor from Gramlib.
Pierre-Marie Pédrot
2018-11-05
Remove Smeta constructor in Gramlib.
Pierre-Marie Pédrot
2018-11-05
[dune] Add to vo rules explicit location of coqlib in boot mode.
Emilio Jesus Gallego Arias
2018-11-05
Merge PR #8899: Remove the deprecated Token module and port the corresponding...
Emilio Jesus Gallego Arias
2018-11-05
Merge PR #8815: NArith: add lemmas about numbers and vectors
Hugo Herbelin
2018-11-05
Merge PR #8871: [library] Move Nametab/Lib specific-names to Nametab
Hugo Herbelin
2018-11-05
Merge PR #8515: Command driven attributes
Pierre-Marie Pédrot
2018-11-05
Merge PR #8870: Pass native and VM flags to the kernel through environment
Pierre-Marie Pédrot
2018-11-05
Merge PR #7952: Fix an algorithmic issue in the vernac guardedness checker.
Gaëtan Gilbert
2018-11-05
Merge PR #8896: Expose Typing.judge_of_apply
Pierre-Marie Pédrot
2018-11-05
Merge PR #8866: Check universe instances in Typing
Pierre-Marie Pédrot
[next]