aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | We do up to `Term` which is the main bulk of the changes.
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | This will allow to merge back `Names` with `API.Names`
* Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.Gravatar Maxime Dénès2017-11-06
|\
* \ Merge PR #6072: Protecting evar map printerGravatar Maxime Dénès2017-11-06
|\ \
* \ \ Merge PR #6074: Refining PR#924 (insensitivity of projection heuristics to ↵Gravatar Maxime Dénès2017-11-06
|\ \ \ | | | | | | | | | | | | alphabet).
* \ \ \ Merge PR #6085: Update .mailmap with a jkloos aliasGravatar Maxime Dénès2017-11-06
|\ \ \ \
* \ \ \ \ Merge PR #6063: Finish removing Show Goal uidGravatar Maxime Dénès2017-11-06
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6049: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" ↵Gravatar Maxime Dénès2017-11-06
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | rules
* \ \ \ \ \ \ Merge PR #1139: Add a linter.Gravatar Maxime Dénès2017-11-06
|\ \ \ \ \ \ \
| | | | * | | | Update .mailmap with a jkloos aliasGravatar Jason Gross2017-11-05
| |_|_|/ / / / |/| | | | | |
| | | | * | | Refining PR#924 (insensitivity of projection heuristics to alphabet).Gravatar Hugo Herbelin2017-11-05
| |_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We refine the criterion for selecting a projection. Before PR#924 it was alphabetic (i.e. morally "random" up to alpha-conversion). After PR#924 it was chronological. We refine a bit more by giving priority to simple projections when they exist over projections which include an evar instantiation (and which may actually be ill-typed).
| | | | * | Cosmetic changes in evar_map printer.Gravatar Hugo Herbelin2017-11-05
| | | | | |
| | | | * | Preventively protect locally against failures of evar_map printer.Gravatar Hugo Herbelin2017-11-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It is not clear that this is really needed, but in case it happens, one will at least have a partial result available rather than an unexploitable global failure of the parser.
| | | | * | Fixing a cause of failure of evar_map printer in debugger.Gravatar Hugo Herbelin2017-11-05
| |_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Indeed, the debugger debugs coqtop but it is itself just an ocaml runtime extended with the coq printers. It does not know the environment, so, looking in the Global.env() for the printers can only fail.
| | | | * [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
| |_|_|/ |/| | | | | | | | | | | This is a first step towards some of the solutions proposed in #6008.
| | | * Finish removing Show Goal uidGravatar Gaëtan Gilbert2017-11-04
| |_|/ |/| | | | | | | | Syntax removed in faa064c746e20a12b3c8f792f69537b18e387be6
* | | Merge PR #6060: Improve error message and fix #6055 (spelling mistake).Gravatar Maxime Dénès2017-11-03
|\ \ \
* \ \ \ Merge PR #6051: Fix FIXME: use OCaml 4.02 generative functors when available.Gravatar Maxime Dénès2017-11-03
|\ \ \ \
* \ \ \ \ Merge PR #6047: A generic printer for ltac valuesGravatar Maxime Dénès2017-11-03
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous ↵Gravatar Maxime Dénès2017-11-03
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | variables).
* \ \ \ \ \ \ Merge PR #6036: [toplevel] Export the last document seen after `Drop`.Gravatar Maxime Dénès2017-11-03
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6031: [ci] Switch back to upstream version of Math-Classes and Corn.Gravatar Maxime Dénès2017-11-03
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in ↵Gravatar Maxime Dénès2017-11-03
|\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | dev/doc/changes.
* \ \ \ \ \ \ \ \ \ Merge PR #6024: Update of Coq version historyGravatar Maxime Dénès2017-11-03
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition).Gravatar Maxime Dénès2017-11-03
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #5999: An attempt to fix issue #5771 (error color hidden by warning ↵Gravatar Maxime Dénès2017-11-03
|\ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | color in coqide).
* \ \ \ \ \ \ \ \ \ \ \ \ 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".
| | | | | | | | | * | | 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).
| | | | | | | | * | 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
|\ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 18:04:03 +0000