aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-04-20simplifying "Environ.push_named" functionMatej Kosik
2017-04-20refactoring "Names.DirPath.is_empty" functionMatej Kosik
2017-04-20refactoring "Names.DirPath.compare" functionMatej Kosik
2017-04-20refactoring "Names.DirPath.equal" functionMatej Kosik
2017-04-20correcting a typo in a commentMatej Kosik
2017-04-20[ide] Set Stateid in query pane.Emilio Jesus Gallego Arias
We again remove another user of Stateid.dummy. However, we need to adapt the protocol so `Coq.query` takes the `route_id` and we can redirect the output properly to the subwindow.
2017-04-19[ide] Rely less on `Stateid.dummy`Emilio Jesus Gallego Arias
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.
2017-04-19Documenting EConstr for developpers.Pierre-Marie Pédrot
2017-04-19Fix bug #5476: Ltac has an inconsistent view of hypotheses.Pierre-Marie Pédrot
2017-04-19Merge PR#573: [toplevel] Fix printing of parsing errors + corner case.Maxime Dénès
2017-04-19CHANGES entry for #545.Maxime Dénès
2017-04-19Merge PR#545: Add some hints to the "real" database to automatically ↵Maxime Dénès
discharge literal comparisons.
2017-04-19Merge PR#538: Correction of bug #4306Maxime Dénès
2017-04-19Merge PR#570: Adding and fixing links in README.Maxime Dénès
2017-04-19Merge PR#571: [toplevel] Fix #5475Maxime Dénès
2017-04-19[toplevel] Fix printing of parsing errors + corner case.Emilio Jesus Gallego Arias
PR #441 and #530 had an interesting interaction creating two bugs: - #441 stopped emitting feedback for the parser, however #530 changed the mechanism to print parser errors to the feedback, thus when the two patches were applied, parsing errors were not printed in batch_mode. - Additionally, #530 contains an error: prior to `Stm.init` we must take care of exceptions `require ()`/etc... otherwise they won't get printed.
2017-04-18[toplevel] Fix #5475Emilio Jesus Gallego Arias
This was a logic error in 63cfc77ddf3586262d905dc351b58669d185a55e, `Notice`-level messages should not be wrapped in `<infomsg>` tags.
2017-04-18Replacing costly merges in UGraph.Pierre-Marie Pédrot
2017-04-18Adding and fixing links in README.Théo Zimmermann
2017-04-17Add a test for bug #5321: clearbody breaks typing of goal.Pierre-Marie Pédrot
The bug has been solved as a side-effect of the EConstr branch.
2017-04-15Merge branch 'v8.6' into trunkMaxime Dénès
2017-04-15Merge PR#523: [readme] Add badges for Travis and Gitter.Maxime Dénès
2017-04-14Fixing bug #5470 (anomaly on notations with misused "binder" type).Hugo Herbelin
2017-04-14Fixing bug #5469 (notation format not recognizing curly braces).Hugo Herbelin
2017-04-14Fix EOL characters in xml protocol documentation.Maxime Dénès
2017-04-14Merge PR#556: Fix anomaly when doing [all:Check _.] during a proof.Maxime Dénès
2017-04-14Fix anomaly when doing [all:Check _.] during a proof.Gaetan Gilbert
2017-04-14Merge PR#557: [toplevel] Don't print goals if there is no pending proof.Maxime Dénès
2017-04-14Merge PR#554: Update INSTALL now that -debug is the default.Maxime Dénès
2017-04-14Merge PR#563: add XML protocol doc for 8.6Maxime Dénès
2017-04-14[travis] Use the lite target for fiat-crypto.Maxime Dénès
2017-04-14Merge PR#559: Fix compilation with camlp5 transitional mode.Maxime Dénès
2017-04-14Fix compilation with camlp5 transitional mode.Maxime Dénès
It was failing after 1d0eb5d4d6fea.
2017-04-13update XML protocol doc to 8.6Paul Steckler
2017-04-13add XML protocol doc for 8.5Paul Steckler
2017-04-13Reinstate 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-13Using 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-13Adding 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-13Silence a few OCaml warnings.Guillaume Melquiond
2017-04-12Merge PR#510: Correctly identify [Time Defined.] as a definedMaxime Dénès
2017-04-12Merge PR#441: Port Toplevel to the Stm APIMaxime Dénès
2017-04-12[toplevel] [stm] cleanup in module openEmilio 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 cleanupEmilio 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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 12:24:00 +0000