Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge PR #7932: CoqIDE scrolls the proof buffer down to the first goal. | 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 | |
|\ \ \ \ | |||
* \ \ \ \ | 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 | |
| |/ / / / |/| | | | | |||
* | | | | | 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 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | * | | | Add overlay for elpi | 2018-06-26 | |
| | | | | | | | | * | | | Remove Sorts.contents | 2018-06-26 | |
| | | | | | | | | |/ / | |||
| | | | | | * | | | | | Add overlay for Equations, Elpi | 2018-06-26 | |
| | | | | | * | | | | | universes_of_constr don't include universes of monomorphic constants | 2018-06-26 | |
* | | | | | | | | | | | Merge PR #7851: Modernize the introduction of the reference manual. | 2018-06-26 | |
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | |||
| | | | | * | | | | | | Activate the build of Ltac2 and Equations in the Windows installer. | 2018-06-25 | |
| | | | | * | | | | | | Reuse CI info to know which version of plugins to build on Windows. | 2018-06-25 | |
* | | | | | | | | | | | Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub... | 2018-06-25 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | * | | Clarify the message "this hint will only be used by eauto" | 2018-06-25 | |
| |_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | |||
| | | | | | * | | | | | Fix for issue 7707: include Ltac2 and Equations in Windows build | 2018-06-25 | |
* | | | | | | | | | | | Merge PR #7559: Existing Class noop when already a class + warning. | 2018-06-25 | |
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / / / |/| | | | | | | | | | | |||
| | | | * | | | | | | | Fix equality check on global names from native compute. | 2018-06-25 | |
| |_|_|/ / / / / / / |/| | | | | | | | | | |||
* | | | | | | | | | | Merge PR #7620: [ssr] rewrite: turn anomaly into regular error | 2018-06-25 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #7895: Revert "Add a note about [ci skip] in CI README." | 2018-06-24 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7805: Towards listing the critical bugs of the history of Coq. | 2018-06-24 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7772: [native_compute] Delay computations with toplevel match | 2018-06-24 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | * | Documenting the syntax of mutual keywords. | 2018-06-24 | |
| | | | | | | | | | | | | * | Added mention of mutual records to CHANGES. | 2018-06-24 | |
| | | | | | | | | | | | | * | Adding various tests for mutual records. | 2018-06-24 | |
| | | | | | | | | | | | | * | Handle mutual record at the vernac level. | 2018-06-24 | |
| | | | | | | | | | | | | * | Handle mutual records in upper layers. | 2018-06-24 | |
| |_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | |||
* | | | | | | | | | | | | | Merge PR #7784: Remove Tutorials from a few other places following #7466. | 2018-06-24 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7614: Simplify the code that handles trust of side-effects in kerne... | 2018-06-23 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7236: [ssr] simpler semantics for delayed clears | 2018-06-23 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7827: [engine] safe [add_unification_pb] interface | 2018-06-23 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7750: Handle mutual records in the kernel | 2018-06-23 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * | | | | | | | | | | | | | | | | | Adapt the kernel to generate proper data for mutual records. | 2018-06-23 | |
| * | | | | | | | | | | | | | | | | | Using more general information for primitive records. | 2018-06-23 |