| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Splitting primitive numeral parser/printer for positive, N, Z into three files. |  Hugo Herbelin | 2018-06-29 |
| * | Merge PR #7860: Fix #7704: Launching coqide through PATH fails. |  Emilio Jesus Gallego Arias | 2018-06-28 |
| |\ | |||
| * \ | Merge PR #7948: Syntax for naming an existential variable |  Théo Zimmermann | 2018-06-28 |
| |\ \ | |||
| * \ \ | Merge PR #7928: Fix 'unbound variable' issue on Windows packaging jobs. |  Michael Soegtrop | 2018-06-28 |
| |\ \ \ | |||
| | | * | | wrong sphinx syntax |  Ambroise | 2018-06-28 |
| * | | | | Merge PR #7946: Update maintainers for native/VM files in pretyping | Théo Zimmermann | 2018-06-28 |
| |\ \ \ \ | |||
| | | | * | | Update gallina-extensions.rst | Ambroise | 2018-06-28 |
| | |_|/ / |/| | | | |||
| * | | | | Merge PR #7937: Mention Consortium in README | Théo Zimmermann | 2018-06-28 |
| |\ \ \ \ | |||
| * \ \ \ \ | Merge PR #7917: Critical bugs: added #3243 and Gonthier's bug in lazy machine. | Théo Zimmermann | 2018-06-28 |
| |\ \ \ \ \ | |||
| * \ \ \ \ \ | Merge PR #7932: CoqIDE scrolls the proof buffer down to the first goal. |  Pierre-Marie Pédrot | 2018-06-28 |
| |\ \ \ \ \ \ | |||
| | | | | * | | | Update maintainers for native/VM files in pretyping |  Maxime Dénès | 2018-06-28 |
| | |_|_|/ / / |/| | | | | | |||
| * | | | | | | Merge PR #7866: Implementation of mutual records in the higher strata | Maxime Dénès | 2018-06-28 |
| |\ \ \ \ \ \ | |||
| * \ \ \ \ \ \ | Merge PR #7934: Add mit-plv/bedrock2-ci to CI | Emilio Jesus Gallego Arias | 2018-06-28 |
| |\ \ \ \ \ \ \ | |||
| | * | | | | | | | Add mit-plv/bedrock2-ci to CI |  Andres Erbsen | 2018-06-27 |
| |/ / / / / / / | |||
| * | | | | | | | Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false) | Pierre-Marie Pédrot | 2018-06-27 |
| |\ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR #7939: Turn the CoqProject_file module into a pure ML file | Emilio Jesus Gallego Arias | 2018-06-27 |
| |\ \ \ \ \ \ \ \ | |||
| | | | | | | * | | | Mention Consortium in README | Maxime Dénès | 2018-06-27 |
| * | | | | | | | | | Merge PR #7924: Ad hoc fix for #5696, #7903 (ltac subterms and open subterms ... | Emilio Jesus Gallego Arias | 2018-06-27 |
| |\ \ \ \ \ \ \ \ \ | |||
| | | * | | | | | | | | Slightly less crazy parsing algorithm for CoqProject_file. | Pierre-Marie Pédrot | 2018-06-27 |
| | | * | | | | | | | | Turn CoqProject_file into a normal OCaml file. | Pierre-Marie Pédrot | 2018-06-27 |
| | |/ / / / / / / / |/| | | | | | | | | |||
| | | | | | | | * | | Fix 'unbound variable' issue on Windows packaging jobs. | Théo Zimmermann | 2018-06-27 |
| * | | | | | | | | | Merge PR #7863: Remove Sorts.contents | Pierre-Marie Pédrot | 2018-06-27 |
| |\ \ \ \ \ \ \ \ \ | |||
| | | | * | | | | | | | Test file for #7723 | Maxime Dénès | 2018-06-27 |
| | | | | | * | | | | | CoqIDE scrolls the proof buffer down to the first goal. |  Cyprien Mangin | 2018-06-27 |
| | | | | | | |_|/ / | | | | | |/| | | | |||
| | | | * | | | | | | Fix #7723: vm_compute segfaults with universe polymorphism | Maxime Dénès | 2018-06-27 |
| | | | | |_|_|/ / | | | |/| | | | | |||
| * | | | | | | | | Merge PR #7888: Clarify the message "this hint will only be used by eauto" | Pierre-Marie Pédrot | 2018-06-27 |
| |\ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ | Merge PR #7826: evd: restrict_evar with candidates, can raise NoCandidatesLeft | Hugo Herbelin | 2018-06-26 |
| |\ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / |/| | | | | | | | | |||
| | | | | * | | | | | Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations). | Hugo Herbelin | 2018-06-26 |
| * | | | | | | | | | Merge PR #7906: universes_of_constr don't include universes of monomorphic co... | Pierre-Marie Pédrot | 2018-06-26 |
| |\ \ \ \ \ \ \ \ \ | |_|_|_|_|/ / / / |/| | | | | | | | | |||
| * | | | | | | | | | Merge PR #7775: Fix handling of universe context for expanded program obligat... | Maxime Dénès | 2018-06-26 |
| |\ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ | Merge PR #7831: Fix for issue #7707: include Ltac2 and Equations in Windows b... | Maxime Dénès | 2018-06-26 |
| |\ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #7756: Fix #7608: missing num package in INSTALL documentation. | Maxime Dénès | 2018-06-26 |
| |\ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7783: Move INSTALL.doc to doc/README.md and improve a few things. | Maxime Dénès | 2018-06-26 |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7919: Fix equality check on global names from native compute. | Maxime Dénès | 2018-06-26 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | * | | | | | Add overlay for elpi |  Gaëtan Gilbert | 2018-06-26 |
| | | | | | | | | | * | | | | | Remove Sorts.contents | Gaëtan Gilbert | 2018-06-26 |
| | | | | | | | | | |/ / / / | |||
| | | | | | | * | | | | | | | Add overlay for Equations, Elpi | Gaëtan Gilbert | 2018-06-26 |
| | | | | | | * | | | | | | | universes_of_constr don't include universes of monomorphic constants | Gaëtan Gilbert | 2018-06-26 |
| * | | | | | | | | | | | | | Merge PR #7851: Modernize the introduction of the reference manual. | Maxime Dénès | 2018-06-26 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | |||
| | | | | | * | | | | | | | | Activate the build of Ltac2 and Equations in the Windows installer. | Théo Zimmermann | 2018-06-25 |
| | | | | | * | | | | | | | | Reuse CI info to know which version of plugins to build on Windows. | Théo Zimmermann | 2018-06-25 |
| * | | | | | | | | | | | | | Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub... |  Matthieu Sozeau | 2018-06-25 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | * | | | | Clarify the message "this hint will only be used by eauto" |  Armaël Guéneau | 2018-06-25 |
| | |_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | |||
| | | | | | | * | | | | | | | Fix for issue 7707: include Ltac2 and Equations in Windows build | Michael Soegtrop | 2018-06-25 |
| * | | | | | | | | | | | | | Merge PR #7559: Existing Class noop when already a class + warning. | Matthieu Sozeau | 2018-06-25 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | |||
| | | | | * | | | | | | | | | Fix equality check on global names from native compute. | Pierre-Marie Pédrot | 2018-06-25 |
| | |_|_|/ / / / / / / / / |/| | | | | | | | | | | | |||
| | | | | | | | | | | * | | Critical bugs: added #3243 and Gonthier's bug in lazy machine. | Hugo Herbelin | 2018-06-25 |
| | |_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | |||
| * | | | | | | | | | | | Merge PR #7620: [ssr] rewrite: turn anomaly into regular error | Maxime Dénès | 2018-06-25 |
| |\ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7895: Revert "Add a note about [ci skip] in CI README." | Emilio Jesus Gallego Arias | 2018-06-24 |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7805: Towards listing the critical bugs of the history of Coq. | Théo Zimmermann | 2018-06-24 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |