| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-02 | Remove redundant env argument to Reduction.ccnv | Gaëtan Gilbert | |
| The infos already contain the env. Note that it was only actually used in the 2 lookup_mind lines. | |||
| 2017-10-25 | Merge PR #6009: Master+misc typos dead code etc | Maxime Dénès | |
| 2017-10-25 | Merge PR #6003: Point HoTT back at master, which now supports Coq master | Maxime Dénès | |
| 2017-10-25 | Merge PR #6002: Move bug files to match their new GitHub ID (fixes #6001). | Maxime Dénès | |
| 2017-10-25 | Merge PR #5995: Revert "Add debug output to brew update." | Maxime Dénès | |
| 2017-10-25 | Merge PR #5993: Switch testing branch back to CompCert upstream. | Maxime Dénès | |
| 2017-10-25 | Merge PR #5980: Add AppVeyor badge next to Travis badge. | Maxime Dénès | |
| 2017-10-25 | Merge PR #5971: [travis] Add flambda testing. | Maxime Dénès | |
| 2017-10-24 | Removing dead code which raised questions. | Hugo Herbelin | |
| 2017-10-24 | Typo in comment in tactic_matching.ml. | Hugo Herbelin | |
| 2017-10-24 | An occurrence of set_id which behaves as the identity. | Hugo Herbelin | |
| 2017-10-24 | A missing newline after a comment. | Hugo Herbelin | |
| 2017-10-23 | Point HoTT back at master, which now supports Coq master | Jason Gross | |
| 2017-10-23 | Move bug files to match their new GitHub ID (fixes #6001). | Théo Zimmermann | |
| 2017-10-20 | Revert "Add debug output to brew update." | Théo Zimmermann | |
| This reverts commit c7465d2ecb69e64613dd38b262f5e78ecad99de1. | |||
| 2017-10-20 | Switch testing branch back to CompCert upstream. | Théo Zimmermann | |
| This follows the merge of AbsInt/CompCert#191. | |||
| 2017-10-20 | Merge PR #5989: Handle ∞ in coq-makefile timing test-suite | Maxime Dénès | |
| 2017-10-20 | Merge PR #5984: CI: build lambdaRust (which depends on Iris) rather than ↵ | Maxime Dénès | |
| just Iris | |||
| 2017-10-20 | Merge PR #5978: Bugzilla autolink: avoid linking inside links (fix #5974). | Maxime Dénès | |
| 2017-10-20 | Merge PR #5972: Fixing link to GitHub issue search, and wording. | Maxime Dénès | |
| 2017-10-20 | Merge PR #1155: Use type nonrec in some functor arguments. | Maxime Dénès | |
| 2017-10-20 | Merge PR #1147: Remove GeoProof support. | Maxime Dénès | |
| 2017-10-20 | Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" ↵ | Maxime Dénès | |
| clause of an inductive definitions | |||
| 2017-10-20 | Merge PR #1095: [stm] Remove state handling from Futures | Maxime Dénès | |
| 2017-10-20 | Merge PR #960: Uniformize references to Bugzilla | Maxime Dénès | |
| 2017-10-19 | rename ci-iris-coq -> ci-iris-lambda-rust | Ralf Jung | |
| 2017-10-19 | Handle ∞ in coq-makefile timing test-suite | Jason Gross | |
| This should (hopefully) fix #5675. | |||
| 2017-10-19 | Moving bug numbers to BZ# format in the CHANGES file. | Théo Zimmermann | |
| Compared to the original proposition (ba7fa6b in #960), this commit only re-formats bug numbers that are also PR numbers. | |||
| 2017-10-19 | Moving bug numbers to BZ# format in the source code. | Théo Zimmermann | |
| Compared to the original proposition (01f848d in #960), this commit only changes files containing bug numbers that are also PR numbers. | |||
| 2017-10-19 | Moving bug numbers to BZ# format in the test-suite. | Théo Zimmermann | |
| Compared to the original proposition (59a594b in #960), this commit only changes files containing bug numbers that are also PR numbers. | |||
| 2017-10-19 | CI: build lambdaRust (which depends on Iris) rather than just Iris | Ralf Jung | |
| 2017-10-19 | Add AppVeyor badge next to Travis badge. | Théo Zimmermann | |
| 2017-10-18 | Bugzilla autolink: avoid linking inside links (fix #5974). | Gaëtan Gilbert | |
| 2017-10-18 | Merge PR #984: Handling primitive projections in canonical structures. | Maxime Dénès | |
| 2017-10-18 | Fixing link to GitHub issue search, and wording. | Théo Zimmermann | |
| 2017-10-18 | [travis] Add flambda testing. | Emilio Jesus Gallego Arias | |
| 2017-10-18 | Merge PR #1149: Moving to GitHub issues. | Maxime Dénès | |
| 2017-10-18 | Moving to GitHub issues. | Théo Zimmermann | |
| This commit adds an issue template asking for version and OS information and adapts the contributing guide to the change of bug tracker. | |||
| 2017-10-17 | Adding a test for bug BZ#5692. | Pierre-Marie Pédrot | |
| 2017-10-17 | unification: fix BZ#5692, recognize prim projs as CS projections | Matthieu Sozeau | |
| 2017-10-17 | Properly handling projection parameters in canonical structures. | Pierre-Marie Pédrot | |
| 2017-10-17 | Handling primitive projections in canonical structures. | Pierre-Marie Pédrot | |
| 2017-10-17 | [vernac] [state] Cache freeze/unfreeze | Emilio Jesus Gallego Arias | |
| Users need to be careful wrt global state modification outside `Vernacentries` without registering the functions. In particular, our fail implementation also has to invalidate the cache. | |||
| 2017-10-17 | [stm] Remove state-handling from Futures. | Emilio Jesus Gallego Arias | |
| We make Vernacentries.interp functional wrt state, and thus remove state-handling from `Future`. Now, a future needs a closure if it wants to preserve state. Consequently, `Vernacentries.interp` takes a state, and returns the new one. We don't explicitly thread the state in the STM yet, instead, we recover the state that was used before and pass it explicitly to `interp`. I have tested the commit with the files in interactive, but we aware that some new bugs may appear or old ones be made more apparent. However, I am confident that this step will improve our understanding of bugs. In some cases, we perform a bit more summary wrapping/unwrapping. This will go away in future commits; informal timings for a full make: - master: real 2m11,027s user 8m30,904s sys 1m0,000s - no_futures: real 2m8,474s user 8m34,380s sys 0m59,156s | |||
| 2017-10-17 | [stm] Move interpretation state to Vernacentries | Emilio Jesus Gallego Arias | |
| We still don't thread the state there, but this is a start of the needed infrastructure. | |||
| 2017-10-17 | [stm] Remove VtBack from public classification. | Emilio Jesus Gallego Arias | |
| We interpret meta-commands directly, instead of going by an intermediate "classifier step". The code could still use some further refactoring, in particular, the `part_of_script` bit is a bit strange likely coming from some special treatment of `VtMeta` in the `query` call, and should go away. | |||
| 2017-10-17 | [stm] First step to move interpretation of Undo commands out of the classifier. | Emilio Jesus Gallego Arias | |
| The vernacular classifier has a current special case for "Undo" like commands, as it needs access to the document structure in order to produce the proper "VtBack" classification, however the classifier is defined before the document is. We introduce a new delegation status `VtMeta` that allows us to interpreted such commands outside the classifier itself. | |||
| 2017-10-16 | Merge PR #1153: [stdlib] Fix warnings on deprecated `Add Setoid` | Maxime Dénès | |
| 2017-10-16 | Use type nonrec in some functor arguments. | Gaëtan Gilbert | |
| 2017-10-16 | Merge PR #1152: Fix BZ#5785 (make install -j broken) | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |