| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-04-13 | update XML protocol doc to 8.6 | Paul Steckler | |
| 2017-04-13 | add XML protocol doc for 8.5 | Paul Steckler | |
| 2017-04-13 | Reinstate fixpoint refolding in [cbn], deactivated by mistake. | Matthieu Sozeau | |
| Add a test-suite file to be sure we won't regress silently. | |||
| 2017-04-13 | [toplevel] Don't print goals if there is no pending proof. | Emilio Jesus Gallego Arias | |
| 2017-04-13 | Using fold_glob_constr_with_binders to code bound_glob_vars. | Hugo Herbelin | |
| To use the generic combinator, we introduce a side effect. I believe that we have more to gain from a short code than from being purely functional. This also fixes the expected semantics since the variables binding the return type in "match" were not taking into account. | |||
| 2017-04-13 | Adding a fold_glob_constr_with_binders combinator. | Hugo Herbelin | |
| Binding generalizable_vars_of_glob_constr, occur_glob_constr, free_glob_vars, and bound_glob_vars on it. Most of the functions of which it factorizes the code were bugged with respect to bindings in the return clause of "match" and in either the types or the bodies of "fix/cofix". | |||
| 2017-04-13 | Silence a few OCaml warnings. | Guillaume Melquiond | |
| 2017-04-12 | Merge PR#510: Correctly identify [Time Defined.] as a defined | Maxime Dénès | |
| 2017-04-12 | Merge PR#441: Port Toplevel to the Stm API | Maxime Dénès | |
| 2017-04-12 | [toplevel] [stm] cleanup in module open | Emilio Jesus Gallego Arias | |
| 2017-04-12 | [stm] [nit] Centralize compile-time debug flag. | Emilio Jesus Gallego Arias | |
| 2017-04-12 | [stm] Improve error messages on add/parse. | Emilio Jesus Gallego Arias | |
| As suggested by @psteckler in #524 , we give more explicit information about what is wrong. We also provide some debug information for the possible dangerous case of having the tip go out of sync with the real installed state (which will make parsing fail if there was some changes to the parser). We also fix a couple of typos noticed by Paul, thanks Paul. | |||
| 2017-04-12 | [flags] Documentation and a minor tweak. | Emilio Jesus Gallego Arias | |
| Mostly documentation and making a couple of local flags, local. | |||
| 2017-04-12 | [vernac] vernacentries.mli cleanup | Emilio Jesus Gallego Arias | |
| This header file had accumulated quite a bit of cruft over the years, we clean it up while we are at it. No functional change as all the removed variables/methods were noops long time ago. | |||
| 2017-04-12 | [stm] Port the toplevel to the STM. | Emilio Jesus Gallego Arias | |
| - We clean-up `Vernac` and make it use the STM API. - Now functions in `Vernac` for use in the toplevel and compiler take an starting `Stateid.t`. - Duplicated `Stm.interp` entry point is removed. - The XML protocol call `interp` is disabled. | |||
| 2017-04-12 | [stm] Move main parsing entry point to the STM. | Emilio Jesus Gallego Arias | |
| Mainly due to notations, proof modes and plugins, parsing in Coq is stateful, so we expose a state-aware parsing API in the STM. This is a first move to unify all the parsing entry points in the Stm and the toplevel, and allows STM clients to control their input stream properly. This greatly helps for instance, with whole-document parsing. This commit supersedes PR#204. | |||
| 2017-04-12 | [stm] Remove edit_id. | Emilio Jesus Gallego Arias | |
| We remove `edit_id` from the STM. In PIDE they serve a different purpose, however in Coq they were of limited utility and required many special cases all around the code. Indeed, parsing is not an asynchronous operation in Coq, thus having feedback about parsing didn't make much sense. All clients indeed ignore such feedback and handle parsing in a synchronous way. XML protocol clients are unaffected, they rely on the instead on the Fail value. This commit supersedes PR#203. | |||
| 2017-04-12 | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵ | Maxime Dénès | |
| record fields. | |||
| 2017-04-12 | Missing optimization when Kernel Term Sharing is disabled. | Pierre-Marie Pédrot | |
| We don't have to perfom in-place updates because we actually know that there is none on the stack. This should speed up UniMath. | |||
| 2017-04-11 | Merge PR#549: Fast path in weak head reduction of applied atoms. | Maxime Dénès | |
| 2017-04-11 | Update INSTALL now that -debug is the default. | Théo Zimmermann | |
| Also updates the references to debugging documentation. | |||
| 2017-04-11 | Merge PR#543: Sanitize instance interpretation | Maxime Dénès | |
| 2017-04-11 | Update RefMan-pre to mention template polymorphism. | Gaetan Gilbert | |
| 2017-04-11 | Update various comments to use "template polymorphism" | Gaetan Gilbert | |
| Also remove obvious comments. | |||
| 2017-04-11 | Use "template polymorphism" in the documentation. | Gaetan Gilbert | |
| 2017-04-11 | Mention template polymorphism in the documentation. | Gaetan Gilbert | |
| Since About mentions it the doc should as well. | |||
| 2017-04-11 | Merge PR#532: Clean Nsatz implementation. | Maxime Dénès | |
| 2017-04-11 | Merge PR#537: Efficient side-effect abstraction | Maxime Dénès | |
| 2017-04-11 | Merge PR#379: Introducing evar-insensitive constrs | Maxime Dénès | |
| 2017-04-10 | Adding a test for 'rewrite in *' when an evar is solved by side-effect. | Pierre-Marie Pédrot | |
| 2017-04-10 | Adding a test for the correctness of normalization in legacy typeclasses. | Pierre-Marie Pédrot | |
| This is a test for commit 9d1230d484a2cf519f9cd76dc0f37815f3c6339b. | |||
| 2017-04-10 | Documenting the changes introduced by the EConstr branch. | Pierre-Marie Pédrot | |
| 2017-04-10 | Revert "refactoring: Reductionops.contextual_reduction_function type" | Matej Košík | |
| This reverts commit 470d0d56467a3a587dc34f958ffea8259618d1ae. | |||
| 2017-04-10 | Revert "comment: typo" | Matej Košík | |
| This reverts commit cd248e01d6834bc43d733c08b5955c332d2146a6. | |||
| 2017-04-10 | Revert "refactoring: Names.DirPath.equal" | Matej Košík | |
| This reverts commit 0d364f7aa5cee042f0b327966fce35778f3285e0. | |||
| 2017-04-10 | Revert "refactoring: Names.DirPath.compare" | Matej Košík | |
| This reverts commit 7a51d6a94bdd6cc889cd69fa0fbb5c8a655b2b16. | |||
| 2017-04-10 | Revert "refactoring: Names.DirPath.is_empty" | Matej Košík | |
| This reverts commit e180cce2384bacaa5ad5b9d6e15b55de8cc913cc. | |||
| 2017-04-10 | Revert "simplify: Environ.push_named" | Matej Košík | |
| This reverts commit 9394aefa8e519a9e2b1b45659a47d5ff3f15ed16. | |||
| 2017-04-10 | Revert "trivial" | Matej Košík | |
| This reverts commit 28973285f4b9389ed0610b94ba907684214dd279. | |||
| 2017-04-10 | Revert "trivial" | Matej Košík | |
| This reverts commit 9b627431516f2cf88312329def9e0ec5e8605a98. | |||
| 2017-04-10 | Revert "comments: corrected in the Context module" | Matej Košík | |
| This reverts commit 538d8edf708ba049e60e6bc32902ba5fdca720bb. | |||
| 2017-04-10 | comments: corrected in the Context module | Matej Kosik | |
| 2017-04-10 | trivial | Matej Kosik | |
| 2017-04-10 | trivial | Matej Kosik | |
| 2017-04-10 | simplify: Environ.push_named | Matej Kosik | |
| 2017-04-10 | refactoring: Names.DirPath.is_empty | Matej Kosik | |
| 2017-04-10 | refactoring: Names.DirPath.compare | Matej Kosik | |
| 2017-04-10 | refactoring: Names.DirPath.equal | Matej Kosik | |
| 2017-04-10 | comment: typo | Matej Kosik | |
| 2017-04-10 | refactoring: Reductionops.contextual_reduction_function type | Matej Kosik | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |