aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* | | | | | | | | | | | | | | | Merge PR #924: Fixing part of #5669: unification heuristics sensitive to ↵Gravatar Maxime Dénès2017-11-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | alphabet
| | | | | | | | | | | * | | | | | Update tactics.mlGravatar Farzon Lotfi2017-11-02
| |_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | fix spelling mistake. reword message to be in the Present Perfect tense instead of the 3rd person present because action is completed with respect to the theorem not some unknown third person.
| | | | | | | | | * | | | | | | Ltac Debug: exporting env and sigma when needed so that term can be printed.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We do it so as to preserve non-focussing semantics for non-focussing generic arguments. This assumes that the code treats them consistently, which is not enforced statically, but which is reasonable in the sense that when we need a context for printing, we have no other choice as needing a context and we needed one also at interpretation time.
| | | | | | | | | * | | | | | | Binding ltac printing functions to the system of generic printing.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This concerns pr_value and message_of_value. This has a few consequences. For instance, no more ad hoc message "a term" or "a tactic", when not enough information is available for printing, one gets a generic message "a value of type foobar". But we also have more printers, satisfying e.g. request #5786.
| | | | | | | | | * | | | | | | Setting a system to register printers for Ltac values.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The model provides three kinds of printers depending on whether the printer needs a context, and, if yes if it supports levels. In the latter case, it takes defaults levels for printing when in a surrounded context (lconstr style) and for printing when not in a surrounded context (constr style). This model preserves the 8.7 focussing semantics of "idtac" (i.e. focussing only when an env is needed) but it also shows that the semantics of "idtac", which focusses the goal depending on the type of its arguments, is a bit ad hoc to understand. See discussion at PR#6047 "https://github.com/coq/coq/pull/6047#discussion_r148278454".
| | | | | | | | | * | | | | | | Exporting ValTMap for use in Genintern.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | Using a specific function to register vernac printers.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | Exporting the level-parametric printer of constr and its variants.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is for eventually being reused in Ltac messages ("idtac").
| | | | | | | | | * | | | | | | Do not identify a pre_ident as a string Ltac value.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It should be printed without quotes and it already has its interpretation function.
| | | | | | | | | * | | | | | | Removing a redundancy in naming types (Ppconstr.precedence = tolerability).Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | Naming the type of Dyn.Map for future reuse.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | Exporting a few more printing functions.Gravatar Hugo Herbelin2017-11-02
| | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | Improving checks about the list separator in tactic notations.Gravatar Hugo Herbelin2017-11-02
| |_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In Tactic Notation and TACTIC EXTEND, when an argument not ending with "_list_sep" was given with a separator, the separator was silently ignored. Now: - we take it into account if it is a list (i.e. ending with "_list"), as if "_list_sep" was given, since after all, the "_sep" is useless in the name. - we fail if there is a separator but it is not a "_list" or "_list_sep".
| | | | | | | | | | | | | | * [API] Some reordering following latest separation commits.Gravatar Emilio Jesus Gallego Arias2017-11-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We can now place most of intf modules just after `Libnames/Globnames` which is quite low on the hierarchy. A exception is `Vernacexpr` which still depends on `Extend` and `GOptions`.
| | | | | | | | | | | | | | * [general] Move Tactypes to `interp`Gravatar Emilio Jesus Gallego Arias2017-11-01
| |_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This makes sense here as the main client is `Stdargs`. This helps with the concerns @herbelin had in https://github.com/coq/coq/issues/6008#issuecomment-341107793
| | | | | | | | | * | | | | Fix FIXME: use OCaml 4.02 generative functors when available.Gravatar Gaëtan Gilbert2017-11-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 4.02.3 has been the minimal OCaml version for a while now.
| | | | | | | | | | | * | | provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rulesGravatar Matej Košík2017-11-01
| |_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Originally, it was not possible to define a new vernacular command in the following way: VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY [ "SomeCmd" ] -> [ Feedback.msg_notice ?loc (Pp.str "some message") ] END because "loc : Loc.t" was not bound. This commit fixes that, i.e. the location of the custom Vernacular command (within *.v file) is made available as "loc" variable bound on the right side of "->" .
| | | * | | | | | | | | | Fixing #2881 ("change with" failing in an Ltac definition).Gravatar Hugo Herbelin2017-10-30
| | | | |_|_|_|_|/ / / / | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We fix by interpreting the pattern in "change pat with term" in strict mode by using the same interning code as for "match goal" (even if the pattern is dropped afterwards).
| | | | | | | | | | | * [ci] Switch VST back to upstream.Gravatar Théo Zimmermann2017-10-30
| | | | | | | |_|_|_|/ | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | This finally closes #5994.
| | | | | | | | * | | Fixing #5401 (printing of patterns with bound anonymous variables).Gravatar Hugo Herbelin2017-10-28
| |_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes also #5731, #6035, #5364.
| | | | | | | * | | [toplevel] Export the last document seen after `Drop`.Gravatar Emilio Jesus Gallego Arias2017-10-28
| | | | |_|_|/ / / | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After `Drop`, `Coqtop.drop_last_doc` will contain the current document used by `Coqloop`. This is useful for people wanting to restart Coq after a `Drop`.
| | | | | | * | | [ci] Switch back to upstream version of Math-Classes and Corn.Gravatar Théo Zimmermann2017-10-27
| | | | |_|/ / / | | | |/| | | |
| | | | | * | | Mention the migration from Bugzilla to GitHub issues in dev/doc/changes.Gravatar Théo Zimmermann2017-10-27
| | | | |/ / / | | | |/| | |
* | | | | | | Merge PR #6026: [ocaml] [travis] Add preliminary 4.06 CI testing.Gravatar Maxime Dénès2017-10-27
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6015: [general] Remove Econstr dependency from `intf`Gravatar Maxime Dénès2017-10-27
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631Gravatar Maxime Dénès2017-10-27
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #5979: Fix #5763: Strictly positive example is out of order.Gravatar Maxime Dénès2017-10-27
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #1113: Adding 3 Arith/QArith lemmas that I found usefulGravatar Maxime Dénès2017-10-27
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #677: Trunk+abstracting injection flagsGravatar Maxime Dénès2017-10-27
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | |
| | * | | | | | | | | | Chaining two tactics in a proofGravatar Raphaël Monat2017-10-27
| | | | | | | | | | | |
| | | | | | * | | | | | [ocaml] [travis] Add preliminary 4.06 CI testing.Gravatar Emilio Jesus Gallego Arias2017-10-27
| |_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We are still missing an updated LABLGTK.
| * | | | | | | | | | Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281.
| * | | | | | | | | | Delay use of flag "Discriminate Introduction" from interp to execution time.Gravatar Hugo Herbelin2017-10-26
| | | | | | | | | | |
| | | | | | | | * | | Updating version history wrt 8.7.Gravatar Hugo Herbelin2017-10-26
| | | | | | | | | | |
| | | | | | | | * | | Updating version history wrt 8.6.Gravatar Hugo Herbelin2017-10-26
| | | | | | | | | | |
| | | | | | | | * | | Updating version history wrt 8.5.Gravatar Hugo Herbelin2017-10-26
| |_|_|_|_|_|_|/ / / |/| | | | | | | | |
| | | * | | | | | | Rename \Tree to \NatTreeGravatar Johannes Kloos2017-10-25
| | | | | | | | | |
| | | | | * | | | | [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
| | |_|_|/ / / / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | To this extent we factor out the relevant bits to a new file, ltac_pretype.
| | * | | | | | | Moving from `is_true` to `= true`Gravatar Raphaël Monat2017-10-25
| | | | | | | | |
| | | | | | | * | Put linter at the top of the tests.Gravatar Théo Zimmermann2017-10-25
| | | | | | | | |
| | | | | | | * | Linter: check that files end with newlines.Gravatar Gaëtan Gilbert2017-10-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We use git check-attr to look at the same files as git diff --check.
| | | | | | | * | Put newlines at the end of files.Gravatar Gaëtan Gilbert2017-10-25
| | | | | | | | |
| | | | | | | * | Add linter.Gravatar Gaëtan Gilbert2017-10-25
| | | | | | | | |
* | | | | | | | | Merge PR #6009: Master+misc typos dead code etcGravatar Maxime Dénès2017-10-25
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6003: Point HoTT back at master, which now supports Coq masterGravatar Maxime Dénès2017-10-25
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6002: Move bug files to match their new GitHub ID (fixes #6001).Gravatar Maxime Dénès2017-10-25
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #5995: Revert "Add debug output to brew update."Gravatar Maxime Dénès2017-10-25
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #5993: Switch testing branch back to CompCert upstream.Gravatar Maxime Dénès2017-10-25
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #5980: Add AppVeyor badge next to Travis badge.Gravatar Maxime Dénès2017-10-25
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #5971: [travis] Add flambda testing.Gravatar Maxime Dénès2017-10-25
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 03:07:28 +0000