aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-04-27contracting the type of "Pfedit.solve_by_implicit_tactic"Matej Košík
2017-04-25Fix an optimization failure in tclPROGRESS.Pierre-Marie Pédrot
Due to code reworking, a fastpath got anihilated because the slow path was computed altogether. We now only compute the slow check whenever the quick one fails.
2017-04-25Merge PR#578: Fix nsatz not recognizing real literals.Maxime Dénès
2017-04-24Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Maxime Dénès
2017-04-24Merge PR#574: Fix bug #5476: Ltac has an inconsistent view of hypotheses.Maxime Dénès
2017-04-24Merge PR#552: Miscelaneous commitsMaxime Dénès
2017-04-24Merge PR#569: Documenting EConstr for developpers.Maxime Dénès
2017-04-24Merge PR#565: Remove VernacErrorMaxime Dénès
2017-04-24Merge PR#580: [ide] Fix #5482 "location for query commands" in IDE.Maxime Dénès
2017-04-24Merge PR#581: [toplevel] [emacs] Don't quote errors in emacs mode.Maxime Dénès
2017-04-24Merge PR#492: [travis] Pin camlp5 to the minimal version 6.14 for 4.02.3Maxime Dénès
2017-04-24Merge PR#576: [ide] Rely less on `Stateid.dummy`Maxime Dénès
2017-04-24[travis] Pin camlp5 to the minimal version 6.14 for 4.02.3Emilio Jesus Gallego Arias
We now test: - 4.02.3 + 6.14 [and 32bits of those] - 4.04.0 + 6.17 this looks like what the official support set should be for 8.7, given that both Ubuntu and Debian will ship the first, then switch to the latter. We also pin xmlm to version 1.2.0 to workaround bug https://github.com/ocaml/opam-repository/issues/8815
2017-04-23[toplevel] [emacs] Don't quote errors in emacs mode.Emilio Jesus Gallego Arias
In 8.6 + emacs, errors were quoted sometimes with special markers (e.g. `Print Module foo.` for a non-existing `foo`) In 8.7 we uniformized error handling and now all errors are quoted, however, this behavior confuses emacs as it seems that the quotes are meant to be applied only to warnings. We thus reflect the de-facto situation, removing quoting for errors and updating the code so it is clear that the quoter is a warnings quoter. We also update the warnings quoter to use a warning tag instead of a non-printable char. This fixes ProofGeneral for trunk users. c.f. https://github.com/ProofGeneral/PG/issues/175
2017-04-22Merge branch v8.6 into trunkHugo Herbelin
Note: I removed what seemed to be dead code in recdef.ml (local_assum and local_def introduced with econstr branch), assuming that this is what should be done.
2017-04-22Removing TODO file which is unused for more than 10 years.Hugo Herbelin
Hoping this is ok for everyone, otherwise we can discuss about it.
2017-04-21[ide] Fix #5482 "location for query commands" in IDE.Emilio Jesus Gallego Arias
This warning is a special case as it happens outside the execution context. We could move the check inside, but instead we opt for the simpler solution of properly setting the warning target.
2017-04-21Remove VernacErrorGaetan Gilbert
2017-04-21[flags] Deprecate is_silent/is_verbose in favor of single flag.Emilio Jesus Gallego Arias
Today, both modes are controlled by a single flag, however this is a bit misleading as is_silent really means "quiet", that is to say `coqc -q` whereas "verbose" is Coq normal operation. We also restore proper behavior of goal printing in coqtop on quiet mode, thanks to @Matafou for the report.
2017-04-20Fix nsatz not recognizing real literals.Guillaume Melquiond
2017-04-20COMMENT: Pre_env.envMatej Kosik
2017-04-20COMMENT: Proof_global.pstate.pidMatej Kosik
2017-04-20refactoring "Ppvernac.pr_extend"Matej Kosik
2017-04-20correcting a typo in a commentMatej Kosik
2017-04-20correcting comments in the "Context" moduleMatej Kosik
2017-04-20"tclENV" is sexier, use it instead of "Env.get"Matej Kosik
2017-04-20reduce syntactic noiseMatej Kosik
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 01:30:54 +0000