aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| | | | | * | | [toplevel] Don't mask critical exceptions in vernac interpretation.Gravatar Emilio Jesus Gallego Arias2017-04-24
| |_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Indeed we were not correctly backtracking in the case of StackOverflow. It makes sense to remove the inner handler which is a leftover of a previous attempt, and handle interpretation errors in load as non-recoverable. This fixes: https://coq.inria.fr/bugs/show_bug.cgi?id=5485
| | | | * | | Adding a dedicated travis overlay for fiat-parsers.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | |
| | | | * | | Removing various tactic compatibility layers in core tactics.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | |
| | | | * | | Porting the firstorder plugin to the new tactic API.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | |
| | | | * | | Removing compatibility layer in Leminv.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | |
| | | | * | | Removing tactic compatibility layer in Command.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | |
| | | | * | | Removing tactic compatibility layer in congruence.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | |
| | | | * | | Removing tactic compatibility layer in Micromega.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | |
| | | | * | | Fix the API of the new pf_constr_of_global.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The current implementation was still using continuation passing-style, and furthermore was triggering a focus on the goals. We take advantage of the tactic features instead.
| | | | * | | Removing trivial compatibility layer in refl_omega.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | |
| | | | * | | Porting omega to the new tactic API.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | |
| | | | * | | Removing trivial compatibility layer in omega.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | |
| | | | * | | Porting generalize_dep to the new tactic engine.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | |
| | | | * | | Removing the tclWEAK_PROGRESS tactical.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The only remaining use was applied on the unfold tactic, and the behaviours of tclPROGRESS and tclWEAK_PROGRESS coincide whenever only one goal is produced by their argument tactic.
| | | | * | | Removing the tclNOTSAMEGOAL primitive from the API.Gravatar Pierre-Marie Pédrot2017-04-24
| |_|_|/ / / |/| | | | | | | | | | | | | | | | | The only use in Equality is reimplemented in the new engine.
* | | | | | Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Maxime Dénès2017-04-24
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#574: Fix bug #5476: Ltac has an inconsistent view of hypotheses.Gravatar Maxime Dénès2017-04-24
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR#552: Miscelaneous commitsGravatar Maxime Dénès2017-04-24
|\ \ \ \ \ \ \ \
| | | | | * \ \ \ Merge PR#577: Add bedrock targets src and facade to Travis CIGravatar Maxime Dénès2017-04-24
| | | | | |\ \ \ \
* | | | | | \ \ \ \ Merge PR#569: Documenting EConstr for developpers.Gravatar Maxime Dénès2017-04-24
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR#565: Remove VernacErrorGravatar Maxime Dénès2017-04-24
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR#580: [ide] Fix #5482 "location for query commands" in IDE.Gravatar Maxime Dénès2017-04-24
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#581: [toplevel] [emacs] Don't quote errors in emacs mode.Gravatar Maxime Dénès2017-04-24
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#492: [travis] Pin camlp5 to the minimal version 6.14 for 4.02.3Gravatar Maxime Dénès2017-04-24
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#576: [ide] Rely less on `Stateid.dummy`Gravatar Maxime Dénès2017-04-24
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | | | | | | [travis] Pin camlp5 to the minimal version 6.14 for 4.02.3Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| | | * | | | | | | | | | | | | [toplevel] [emacs] Don't quote errors in emacs mode.Gravatar Emilio Jesus Gallego Arias2017-04-23
| | |/ / / / / / / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* | | | | | | | | | | | | | | Merge branch v8.6 into trunkGravatar Hugo Herbelin2017-04-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | |_|_|_|_|_|_|_|_|/ / / / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | | | | | | | | | Removing TODO file which is unused for more than 10 years.Gravatar Hugo Herbelin2017-04-22
| |_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Hoping this is ok for everyone, otherwise we can discuss about it.
| | | * | | | | | | | | | | [ide] Fix #5482 "location for query commands" in IDE.Gravatar Emilio Jesus Gallego Arias2017-04-21
| |_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | * | | | | | | | | | Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
| |_|/ / / / / / / / / / |/| | | | | | | | | | |
| | | | | | * | | | | | [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | | * | | | Add bedrock targets src and facadeGravatar Jason Gross2017-04-20
| | |_|_|_|_|_|/ / / / | |/| | | | | | | | |
| | | | | | | * | | | Fix nsatz not recognizing real literals.Gravatar Guillaume Melquiond2017-04-20
| |_|_|_|_|_|/ / / / |/| | | | | | | | |
| | | | | | | * | | Fix bug #5377: @? patterns broken.Gravatar Pierre-Marie Pédrot2017-04-20
| | |_|_|_|_|/ / / | |/| | | | | | |
| | | | * | | | | COMMENT: Pre_env.envGravatar Matej Kosik2017-04-20
| | | | | | | | |
| | | | * | | | | COMMENT: Proof_global.pstate.pidGravatar Matej Kosik2017-04-20
| | | | | | | | |
| | | | * | | | | refactoring "Ppvernac.pr_extend"Gravatar Matej Kosik2017-04-20
| | | | | | | | |
| | | | * | | | | correcting a typo in a commentGravatar Matej Kosik2017-04-20
| | | | | | | | |
| | | | * | | | | correcting comments in the "Context" moduleGravatar Matej Kosik2017-04-20
| | | | | | | | |
| | | | * | | | | "tclENV" is sexier, use it instead of "Env.get"Gravatar Matej Kosik2017-04-20
| | | | | | | | |
| | | | * | | | | reduce syntactic noiseGravatar Matej Kosik2017-04-20
| | | | | | | | |
| | | | * | | | | simplifying "Environ.push_named" functionGravatar Matej Kosik2017-04-20
| | | | | | | | |
| | | | * | | | | refactoring "Names.DirPath.is_empty" functionGravatar Matej Kosik2017-04-20
| | | | | | | | |
| | | | * | | | | refactoring "Names.DirPath.compare" functionGravatar Matej Kosik2017-04-20
| | | | | | | | |
| | | | * | | | | refactoring "Names.DirPath.equal" functionGravatar Matej Kosik2017-04-20
| | | | | | | | |
| | | | * | | | | correcting a typo in a commentGravatar Matej Kosik2017-04-20
| |_|_|/ / / / / |/| | | | | | |
| | * | | | | | [ide] Set Stateid in query pane.Gravatar Emilio Jesus Gallego Arias2017-04-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | | | | [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.
| | | * | | | Documenting EConstr for developpers.Gravatar Pierre-Marie Pédrot2017-04-19
| | |/ / / /
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 05:57:46 +0000