Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Port g_vernac to the homebrew GEXTEND parser. | 2018-06-29 | |
* | Port g_proofs to the homebrew GEXTEND parser. | 2018-06-29 | |
* | Port g_constr to the homebrew GEXTEND parser. | 2018-06-29 | |
* | Port g_prim to the homebrew GEXTEND parser. | 2018-06-29 | |
* | Use a homebrew parser to replace the GEXTEND extension points of Camlp5. | 2018-06-29 | |
* | Merge PR #7918: Mini-update of version history with recent changes. | 2018-06-29 | |
|\ | |||
* \ | Merge PR #7080: Swapping Context and Constr and defining declarations on cons... | 2018-06-29 | |
|\ \ | |||
* \ \ | Merge PR #7890: Inline a function from Quote used in setoid_ring. | 2018-06-29 | |
|\ \ \ | |||
* \ \ \ | Merge PR #7745: Make type Environ.globals abstract + simplify Environ.retrokn... | 2018-06-29 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #7950: Documentation for 8.8.1 | 2018-06-29 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #7860: Fix #7704: Launching coqide through PATH fails. | 2018-06-28 | |
|\ \ \ \ \ \ | |||
| | * | | | | | CHANGES for 8.8.1. | 2018-06-28 | |
| | * | | | | | Self-credit for the work done. | 2018-06-28 | |
| |/ / / / / |/| | | | | | |||
* | | | | | | Merge PR #7948: Syntax for naming an existential variable | 2018-06-28 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #7928: Fix 'unbound variable' issue on Windows packaging jobs. | 2018-06-28 | |
|\ \ \ \ \ \ \ | |||
| | * | | | | | | wrong sphinx syntax | 2018-06-28 | |
* | | | | | | | | Merge PR #7946: Update maintainers for native/VM files in pretyping | 2018-06-28 | |
|\ \ \ \ \ \ \ \ | |||
| | | * | | | | | | Update gallina-extensions.rst | 2018-06-28 | |
| |_|/ / / / / / |/| | | | | | | | |||
* | | | | | | | | Merge PR #7937: Mention Consortium in README | 2018-06-28 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #7917: Critical bugs: added #3243 and Gonthier's bug in lazy machine. | 2018-06-28 | |
|\ \ \ \ \ \ \ \ \ | |||
| | | | | | * | | | | Deprecate Environ.retroknowledge function in favor of the projection | 2018-06-28 | |
| | | | | | * | | | | [env.env_rel_context.env_rel_ctx] -> [rel_context env] | 2018-06-28 | |
| | | | | | * | | | | Make Environ.globals abstract. | 2018-06-28 | |
| |_|_|_|_|/ / / / |/| | | | | | | | | |||
* | | | | | | | | | Merge PR #7932: CoqIDE scrolls the proof buffer down to the first goal. | 2018-06-28 | |
|\ \ \ \ \ \ \ \ \ | |||
| | | | * | | | | | | Update maintainers for native/VM files in pretyping | 2018-06-28 | |
| |_|_|/ / / / / / |/| | | | | | | | | |||
* | | | | | | | | | Merge PR #7866: Implementation of mutual records in the higher strata | 2018-06-28 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #7934: Add mit-plv/bedrock2-ci to CI | 2018-06-28 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| * | | | | | | | | | | Add mit-plv/bedrock2-ci to CI | 2018-06-27 | |
|/ / / / / / / / / / | |||
* | | | | | | | | | | Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false) | 2018-06-27 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #7939: Turn the CoqProject_file module into a pure ML file | 2018-06-27 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | * | | | | | | Mention Consortium in README | 2018-06-27 | |
| | | | | | | | | | * | | Adding overlay. | 2018-06-27 | |
| | | | | | | | | | * | | Swapping Context and Constr: defining declarations on constr in Constr. | 2018-06-27 | |
| |_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | |||
* | | | | | | | | | | | Merge PR #7924: Ad hoc fix for #5696, #7903 (ltac subterms and open subterms ... | 2018-06-27 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
| | * | | | | | | | | | | Slightly less crazy parsing algorithm for CoqProject_file. | 2018-06-27 | |
| | * | | | | | | | | | | Turn CoqProject_file into a normal OCaml file. | 2018-06-27 | |
| |/ / / / / / / / / / |/| | | | | | | | | | | |||
| | | | | | | * | | | | Fix 'unbound variable' issue on Windows packaging jobs. | 2018-06-27 | |
* | | | | | | | | | | | Merge PR #7863: Remove Sorts.contents | 2018-06-27 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
| | | * | | | | | | | | | Test file for #7723 | 2018-06-27 | |
| | | | | * | | | | | | | CoqIDE scrolls the proof buffer down to the first goal. | 2018-06-27 | |
| | | | | | |_|/ / / / | | | | | |/| | | | | | |||
| | | * | | | | | | | | Fix #7723: vm_compute segfaults with universe polymorphism | 2018-06-27 | |
| | | | |_|_|/ / / / | | | |/| | | | | | | |||
* | | | | | | | | | | Merge PR #7888: Clarify the message "this hint will only be used by eauto" | 2018-06-27 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #7826: evd: restrict_evar with candidates, can raise NoCandidatesLeft | 2018-06-26 | |
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / / / |/| | | | | | | | | | | |||
| | | | * | | | | | | | Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations). | 2018-06-26 | |
* | | | | | | | | | | | Merge PR #7906: universes_of_constr don't include universes of monomorphic co... | 2018-06-26 | |
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|/ / / / / / |/| | | | | | | | | | | |||
* | | | | | | | | | | | Merge PR #7775: Fix handling of universe context for expanded program obligat... | 2018-06-26 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7831: Fix for issue #7707: include Ltac2 and Equations in Windows b... | 2018-06-26 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7756: Fix #7608: missing num package in INSTALL documentation. | 2018-06-26 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7783: Move INSTALL.doc to doc/README.md and improve a few things. | 2018-06-26 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7919: Fix equality check on global names from native compute. | 2018-06-26 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |