| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-02 | Binding the specialize tactic. | Pierre-Marie Pédrot | |
| 2017-11-02 | Ltac 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-02 | Binding 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-02 | Setting 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-02 | Exporting ValTMap for use in Genintern. | Hugo Herbelin | |
| 2017-11-02 | Using a specific function to register vernac printers. | Hugo Herbelin | |
| 2017-11-02 | Exporting the level-parametric printer of constr and its variants. | Hugo Herbelin | |
| This is for eventually being reused in Ltac messages ("idtac"). | |||
| 2017-11-02 | Do 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-02 | Removing a redundancy in naming types (Ppconstr.precedence = tolerability). | Hugo Herbelin | |
| 2017-11-02 | Naming the type of Dyn.Map for future reuse. | Hugo Herbelin | |
| 2017-11-02 | Exporting a few more printing functions. | Hugo Herbelin | |
| 2017-11-02 | Improving 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-01 | [API] Some reordering following latest separation commits. | Emilio Jesus Gallego Arias | |
| 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`. | |||
| 2017-11-01 | [general] Move Tactypes to `interp` | Emilio Jesus Gallego Arias | |
| 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 | |||
| 2017-11-01 | Fix 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-01 | provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules | Matej 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-30 | Fixing #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-30 | Add a macro for the now tactic | Pierre-Marie Pédrot | |
| 2017-10-30 | Put notations in level 5 by default. | Pierre-Marie Pédrot | |
| 2017-10-30 | Fix the semantics of introducing with empty intro patterns. | Pierre-Marie Pédrot | |
| 2017-10-30 | Introducing the change tactic. | Pierre-Marie Pédrot | |
| 2017-10-30 | Fix compilation after merge of Ltac_pretype interface. | Pierre-Marie Pédrot | |
| 2017-10-30 | [ci] Switch VST back to upstream. | Théo Zimmermann | |
| This finally closes #5994. | |||
| 2017-10-28 | Fixing #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-27 | Mention the migration from Bugzilla to GitHub issues in dev/doc/changes. | Théo Zimmermann | |
| 2017-10-27 | Adding documentation | Pierre-Marie Pédrot | |
| 2017-10-27 | Better printers for toplevel values. | Pierre-Marie Pédrot | |
| 2017-10-27 | Adding an OPAM package. | Pierre-Marie Pédrot | |
| 2017-10-27 | Adding a notation for match goal. | Pierre-Marie Pédrot | |
| 2017-10-27 | Merge PR #6026: [ocaml] [travis] Add preliminary 4.06 CI testing. | Maxime Dénès | |
| 2017-10-27 | Merge PR #6015: [general] Remove Econstr dependency from `intf` | Maxime Dénès | |
| 2017-10-27 | Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631 | Maxime Dénès | |
| 2017-10-27 | Merge PR #5979: Fix #5763: Strictly positive example is out of order. | Maxime Dénès | |
| 2017-10-27 | Merge PR #1113: Adding 3 Arith/QArith lemmas that I found useful | Maxime Dénès | |
| 2017-10-27 | Merge PR #677: Trunk+abstracting injection flags | Maxime Dénès | |
| 2017-10-27 | Adding a command to evaluate Ltac2 expressions. | Pierre-Marie Pédrot | |
| 2017-10-27 | Fix goal_matching quotation. | Pierre-Marie Pédrot | |
| 2017-10-27 | Fix relative meaning of Pattern vs. Context in match goal. | Pierre-Marie Pédrot | |
| 2017-10-27 | Stubs for goal matching: quotation and matching function. | Pierre-Marie Pédrot | |
| 2017-10-27 | Chaining two tactics in a proof | Raphaël Monat | |
| 2017-10-27 | [ocaml] [travis] Add preliminary 4.06 CI testing. | Emilio Jesus Gallego Arias | |
| We are still missing an updated LABLGTK. | |||
| 2017-10-26 | Passing around the flag for injection so that tactics calling inj at | Hugo Herbelin | |
| 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. | |||
| 2017-10-26 | Delay use of flag "Discriminate Introduction" from interp to execution time. | Hugo Herbelin | |
| 2017-10-26 | Updating version history wrt 8.7. | Hugo Herbelin | |
| 2017-10-26 | Updating version history wrt 8.6. | Hugo Herbelin | |
| 2017-10-26 | Updating version history wrt 8.5. | Hugo Herbelin | |
| 2017-10-25 | Rename \Tree to \NatTree | Johannes Kloos | |
| 2017-10-25 | Use GHC.Base.Any for compatibility with GHC 8.2 | Tej Chajed | |
| Fixes #6022. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |