aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* [ide] Rely less on `Stateid.dummy`Gravatar Emilio Jesus Gallego Arias2017-04-19
| | | | | | | | | | | | | In particular, we set queries from the menu to the tip of the document, and process feedback coming with a `dummy` id. There are still more places to tweak, but this should be good for now. We also display a few more query messages, in particular the feedbacks produced by query that carry a dummy state id. This hack of reporting with from the STM should be solved once we update the protocol.
* Add a test for bug #5321: clearbody breaks typing of goal.Gravatar Pierre-Marie Pédrot2017-04-17
| | | | The bug has been solved as a side-effect of the EConstr branch.
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\
* \ Merge PR#523: [readme] Add badges for Travis and Gitter.Gravatar Maxime Dénès2017-04-15
|\ \
| | * Fixing bug #5470 (anomaly on notations with misused "binder" type).Gravatar Hugo Herbelin2017-04-14
| | |
| | * Fixing bug #5469 (notation format not recognizing curly braces).Gravatar Hugo Herbelin2017-04-14
| | |
| | * Fix EOL characters in xml protocol documentation.Gravatar Maxime Dénès2017-04-14
| | |
| | * Merge PR#556: Fix anomaly when doing [all:Check _.] during a proof.Gravatar Maxime Dénès2017-04-14
| | |\
| | | * Fix anomaly when doing [all:Check _.] during a proof.Gravatar Gaetan Gilbert2017-04-14
| | | |
* | | | Merge PR#557: [toplevel] Don't print goals if there is no pending proof.Gravatar Maxime Dénès2017-04-14
|\ \ \ \
* \ \ \ \ Merge PR#554: Update INSTALL now that -debug is the default.Gravatar Maxime Dénès2017-04-14
|\ \ \ \ \
| | | | * \ Merge PR#563: add XML protocol doc for 8.6Gravatar Maxime Dénès2017-04-14
| | | | |\ \
| | | | * | | [travis] Use the lite target for fiat-crypto.Gravatar Maxime Dénès2017-04-14
| | | | | |/ | | | | |/|
* | | | | | Merge PR#559: Fix compilation with camlp5 transitional mode.Gravatar Maxime Dénès2017-04-14
|\ \ \ \ \ \
| * | | | | | Fix compilation with camlp5 transitional mode.Gravatar Maxime Dénès2017-04-14
|/ / / / / / | | | | | | | | | | | | | | | | | | It was failing after 1d0eb5d4d6fea.
| | | | | * update XML protocol doc to 8.6Gravatar Paul Steckler2017-04-13
| | | | | |
| | | | | * add XML protocol doc for 8.5Gravatar Paul Steckler2017-04-13
| | | | |/
| | * | | [toplevel] Don't print goals if there is no pending proof.Gravatar Emilio Jesus Gallego Arias2017-04-13
| | | | |
* | | | | Silence a few OCaml warnings.Gravatar Guillaume Melquiond2017-04-13
| |/ / / |/| | |
| | | * Merge PR#510: Correctly identify [Time Defined.] as a definedGravatar Maxime Dénès2017-04-12
| | | |\
* | | | \ Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\ \ \ \ \
| * | | | | [toplevel] [stm] cleanup in module openGravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | |
| * | | | | [stm] [nit] Centralize compile-time debug flag.Gravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | |
| * | | | | [stm] Improve error messages on add/parse.Gravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | | | [flags] Documentation and a minor tweak.Gravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | | | | | | | | | | | | | | | | | | | | Mostly documentation and making a couple of local flags, local.
| * | | | | [vernac] vernacentries.mli cleanupGravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | | | [stm] Port the toplevel to the STM.Gravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - 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.
| * | | | | [stm] Move main parsing entry point to the STM.Gravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | | | [stm] Remove edit_id.Gravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵Gravatar Maxime Dénès2017-04-12
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | record fields.
* \ \ \ \ \ \ Merge PR#549: Fast path in weak head reduction of applied atoms.Gravatar Maxime Dénès2017-04-11
|\ \ \ \ \ \ \
| | | | * | | | Update INSTALL now that -debug is the default.Gravatar Théo Zimmermann2017-04-11
| |_|_|/ / / / |/| | | | | | | | | | | | | Also updates the references to debugging documentation.
* | | | | | | Merge PR#543: Sanitize instance interpretationGravatar Maxime Dénès2017-04-11
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR#532: Clean Nsatz implementation.Gravatar Maxime Dénès2017-04-11
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR#537: Efficient side-effect abstractionGravatar Maxime Dénès2017-04-11
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR#379: Introducing evar-insensitive constrsGravatar Maxime Dénès2017-04-11
|\ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | Adding a test for 'rewrite in *' when an evar is solved by side-effect.Gravatar Pierre-Marie Pédrot2017-04-10
| | | | | | | | | | |
| * | | | | | | | | | Adding a test for the correctness of normalization in legacy typeclasses.Gravatar Pierre-Marie Pédrot2017-04-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a test for commit 9d1230d484a2cf519f9cd76dc0f37815f3c6339b.
| * | | | | | | | | | Documenting the changes introduced by the EConstr branch.Gravatar Pierre-Marie Pédrot2017-04-10
| | | | | | | | | | |
* | | | | | | | | | | Revert "refactoring: Reductionops.contextual_reduction_function type"Gravatar Matej Košík2017-04-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit 470d0d56467a3a587dc34f958ffea8259618d1ae.
* | | | | | | | | | | Revert "comment: typo"Gravatar Matej Košík2017-04-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit cd248e01d6834bc43d733c08b5955c332d2146a6.
* | | | | | | | | | | Revert "refactoring: Names.DirPath.equal"Gravatar Matej Košík2017-04-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit 0d364f7aa5cee042f0b327966fce35778f3285e0.
* | | | | | | | | | | Revert "refactoring: Names.DirPath.compare"Gravatar Matej Košík2017-04-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit 7a51d6a94bdd6cc889cd69fa0fbb5c8a655b2b16.
* | | | | | | | | | | Revert "refactoring: Names.DirPath.is_empty"Gravatar Matej Košík2017-04-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit e180cce2384bacaa5ad5b9d6e15b55de8cc913cc.
* | | | | | | | | | | Revert "simplify: Environ.push_named"Gravatar Matej Košík2017-04-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit 9394aefa8e519a9e2b1b45659a47d5ff3f15ed16.
* | | | | | | | | | | Revert "trivial"Gravatar Matej Košík2017-04-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit 28973285f4b9389ed0610b94ba907684214dd279.
* | | | | | | | | | | Revert "trivial"Gravatar Matej Košík2017-04-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit 9b627431516f2cf88312329def9e0ec5e8605a98.
* | | | | | | | | | | Revert "comments: corrected in the Context module"Gravatar Matej Košík2017-04-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit 538d8edf708ba049e60e6bc32902ba5fdca720bb.
* | | | | | | | | | | comments: corrected in the Context moduleGravatar Matej Kosik2017-04-10
| | | | | | | | | | |
* | | | | | | | | | | trivialGravatar Matej Kosik2017-04-10
| | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 02:09:05 +0000