aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-11-07[api] Remove 8.7 ML-deprecated functions.Emilio Jesus Gallego Arias
2017-11-06Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.Maxime Dénès
2017-11-06Merge PR #6072: Protecting evar map printerMaxime Dénès
2017-11-06Merge PR #6074: Refining PR#924 (insensitivity of projection heuristics to ↵Maxime Dénès
alphabet).
2017-11-06Merge PR #6085: Update .mailmap with a jkloos aliasMaxime Dénès
2017-11-06Merge PR #6063: Finish removing Show Goal uidMaxime Dénès
2017-11-06Merge PR #6049: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" ↵Maxime Dénès
rules
2017-11-06Merge PR #1139: Add a linter.Maxime Dénès
2017-11-05Update .mailmap with a jkloos aliasJason Gross
2017-11-05Refining PR#924 (insensitivity of projection heuristics to alphabet).Hugo Herbelin
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).
2017-11-05Cosmetic changes in evar_map printer.Hugo Herbelin
2017-11-05Preventively protect locally against failures of evar_map printer.Hugo Herbelin
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.
2017-11-05Fixing a cause of failure of evar_map printer in debugger.Hugo Herbelin
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.
2017-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
This is a first step towards some of the solutions proposed in #6008.
2017-11-04Finish removing Show Goal uidGaëtan Gilbert
Syntax removed in faa064c746e20a12b3c8f792f69537b18e387be6
2017-11-03Merge PR #6060: Improve error message and fix #6055 (spelling mistake).Maxime Dénès
2017-11-03Merge PR #6051: Fix FIXME: use OCaml 4.02 generative functors when available.Maxime Dénès
2017-11-03Merge PR #6047: A generic printer for ltac valuesMaxime Dénès
2017-11-03Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous ↵Maxime Dénès
variables).
2017-11-03Merge PR #6036: [toplevel] Export the last document seen after `Drop`.Maxime Dénès
2017-11-03Merge PR #6031: [ci] Switch back to upstream version of Math-Classes and Corn.Maxime Dénès
2017-11-03Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in ↵Maxime Dénès
dev/doc/changes.
2017-11-03Merge PR #6024: Update of Coq version historyMaxime Dénès
2017-11-03Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition).Maxime Dénès
2017-11-03Merge PR #5999: An attempt to fix issue #5771 (error color hidden by warning ↵Maxime Dénès
color in coqide).
2017-11-03Merge PR #924: Fixing part of #5669: unification heuristics sensitive to ↵Maxime Dénès
alphabet
2017-11-02Update tactics.mlFarzon Lotfi
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.
2017-11-02Ltac Debug: exporting env and sigma when needed so that term can be printed.Hugo Herbelin
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.
2017-11-02Binding ltac printing functions to the system of generic printing.Hugo Herbelin
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.
2017-11-02Setting a system to register printers for Ltac values.Hugo Herbelin
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".
2017-11-02Exporting ValTMap for use in Genintern.Hugo Herbelin
2017-11-02Using a specific function to register vernac printers.Hugo Herbelin
2017-11-02Exporting the level-parametric printer of constr and its variants.Hugo Herbelin
This is for eventually being reused in Ltac messages ("idtac").
2017-11-02Do not identify a pre_ident as a string Ltac value.Hugo Herbelin
It should be printed without quotes and it already has its interpretation function.
2017-11-02Removing a redundancy in naming types (Ppconstr.precedence = tolerability).Hugo Herbelin
2017-11-02Naming the type of Dyn.Map for future reuse.Hugo Herbelin
2017-11-02Exporting a few more printing functions.Hugo Herbelin
2017-11-02Improving checks about the list separator in tactic notations.Hugo Herbelin
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".
2017-11-01Fix FIXME: use OCaml 4.02 generative functors when available.Gaëtan Gilbert
4.02.3 has been the minimal OCaml version for a while now.
2017-11-01provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rulesMatej Košík
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 "->" .
2017-10-30Fixing #2881 ("change with" failing in an Ltac definition).Hugo Herbelin
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).
2017-10-28Fixing #5401 (printing of patterns with bound anonymous variables).Hugo Herbelin
This fixes also #5731, #6035, #5364.
2017-10-28[toplevel] Export the last document seen after `Drop`.Emilio Jesus Gallego Arias
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`.
2017-10-27[ci] Switch back to upstream version of Math-Classes and Corn.Théo Zimmermann
2017-10-27Mention the migration from Bugzilla to GitHub issues in dev/doc/changes.Théo Zimmermann
2017-10-27Merge PR #6026: [ocaml] [travis] Add preliminary 4.06 CI testing.Maxime Dénès
2017-10-27Merge PR #6015: [general] Remove Econstr dependency from `intf`Maxime Dénès
2017-10-27Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631Maxime Dénès
2017-10-27Merge PR #5979: Fix #5763: Strictly positive example is out of order.Maxime Dénès
2017-10-27Merge PR #1113: Adding 3 Arith/QArith lemmas that I found usefulMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 14:42:21 +0000