aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* [located] [doc] Improve docs for `CAst.ast`.Gravatar Emilio Jesus Gallego Arias2017-04-25
|
* [travis] mathcomp and fiat overlay for #402Gravatar Emilio Jesus Gallego Arias2017-04-25
|
* [location] Cleanup.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | We remove some unnecessary functions introduced before in the patch series + unused functions.
* [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
|
* [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | Following @gasche idea, and the original intention of #402, we switch the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast` which is private and record-based. This provides significantly clearer code for the AST, and is robust wrt attributes.
* [location] Be consistent with type module qualificationGravatar Emilio Jesus Gallego Arias2017-04-25
| | | | Thanks to @gasche
* [location] Document changes.Gravatar Emilio Jesus Gallego Arias2017-04-25
|
* [location] Remove `Loc.internal_ghost`Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | `internal_ghost` was an artifact to ease porting of the ml4 rules. Now that the location is optional we can finally get rid of it.
* [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
* [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | Now it is a private field, locations are optional.
* [location] Use located in tactics.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | | One case missing due the TACTIC EXTEND macro.
* [location] Use located in misctypes.Gravatar Emilio Jesus Gallego Arias2017-04-24
|
* [location] More located use.Gravatar Emilio Jesus Gallego Arias2017-04-24
|
* [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
|
* [location] Move Glob_term.predicate_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | | | We continue the uniformization pass. No big news here, trying to be minimally invasive.
* [location] Move Glob_term.cases_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | | | We continue the uniformization pass. No big news here, trying to be minimally invasive.
* [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | | | | | | | This is the second patch, which is a bit more invasive. We reasoning is similar to the previous patch. Code is not as clean as it could as we would need to convert `glob_constr` to located too, then a few parts could just map the location.
* [constrexpr] Make patterns use Loc.located for location informationGravatar Emilio Jesus Gallego Arias2017-04-24
| | | | | | | | | | | | | | | | | | | | | This is first of a series of patches, converting `constrexpr` pattern data type from ad-hoc location handling to `Loc.located`. Along Coq, we can find two different coding styles for handling objects with location information: one style uses `'a Loc.located`, whereas other data structures directly embed `Loc.t` in their constructors. Handling all located objects uniformly would be very convenient, and would allow optimizing certain cases, in particular making located smarter when there is no location information, as it is the case for all terms coming from the kernel. `git grep 'Loc.t \*'` gives an overview of the remaining work to do. We've also added an experimental API for `located` to the `Loc` module, `Loc.tag` should be used to add locations objects, making it explicit in the code when a "located" object is created.
* 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#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.
| | | | * | | 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
| | |/ /
| | | * Fix bug #5476: Ltac has an inconsistent view of hypotheses.Gravatar Pierre-Marie Pédrot2017-04-19
| |_|/ |/| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 13:53:29 +0000