aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Collapse)AuthorAge
...
* | Fixing missing parentheses in printing of patterns in binders.Gravatar Hugo Herbelin2016-07-19
| | | | | | | | (In agreement with Daniel.)
* | primproj: warning and avoid error.Gravatar Matthieu Sozeau2016-07-06
| | | | | | | | | | | | | | | | When defining a (co)recursive inductive with primitive projections on, which lacks eta-conversion and hence dependent elimination, build only the associated non-dependent elimination principles, and warn about this. Also make the printing of the status of an inductive w.r.t. projections and eta conversion explicit in Print and About.
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | | | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* | Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
| |
* | Merge remote-tracking branch 'github/pr/207' into trunkGravatar Maxime Dénès2016-06-28
|\ \ | | | | | | | | | Was PR#207: Add -no-print-dependent-evars
* | | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| | | | | | | | | | | | Cf CHANGES for details.
| * | Add [Unset Printing Dependent Evars Line]Gravatar Jason Gross2016-06-19
|/ / | | | | | | | | This allows a work-around for bug #4819, https://coq.inria.fr/bugs/show_bug.cgi?id=4819.
* | Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
| |
* | Print the type-in-type flag in various user-facing functions.Gravatar Pierre-Marie Pédrot2016-06-18
| |
* | Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
| | | | | | | | | | simplifying and generalizing the grammar entries for injection, discriminate and simplify_eq.
* | Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In pat%constr, creating new evars is now allowed only if "eintros" is given, i.e. "intros" checks that no evars are created, and similarly e.g. for "injection ... as ... pat%constr". The form "eintros [...]" or "eintros ->" with the case analysis or rewrite creating evars is now also supported. This is not a commitment to say that it is good to have an e- modifier to tactics. It is just to be consistent with the existing convention. It seems to me that the "no e-" variants are good for beginners. However, expert might prefer to use the e-variants by default. Opinions from teachers and users would be useful. To be possibly done: do that [= ...] work on hypotheses with side conditions or parameters based on the idea that they apply the full injection and not only the restriction of it to goals which are exactly an equality, as it is today.
* | proof mode: print unification constraintsGravatar Matthieu Sozeau2016-06-16
| | | | | | | | along with goals, with nice formatting.
* | Extend Hint Mode to handle the no-head-evar caseGravatar Matthieu Sozeau2016-06-16
| | | | | | | | | | | | | | Suggested by R. Krebbers and C. Cohen, this makes modes more applicable, by allowing to trigger resolution on partially instantiated indices. This is a rough but fast approximation of the pattern on which one would like instances to apply.
* | Isolating and exporting a function for printing body of a recursive definition.Gravatar Hugo Herbelin2016-06-16
| |
* | Simplification in ppvernac.ml.Gravatar Hugo Herbelin2016-06-16
| |
* | Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.Gravatar Hugo Herbelin2016-06-16
| | | | | | | | No other changes (long only because of a change of indentation).
* | Fixing extra space in printing bullets.Gravatar Hugo Herbelin2016-06-16
| |
* | Fixing space in printing <+ and <: + fixing missing Inline keyword.Gravatar Hugo Herbelin2016-06-16
| | | | | | | | Fixing : in Declare Module.
* | Fixing printing of Instance.Gravatar Hugo Herbelin2016-06-16
| |
* | Fixing extra space in printing abbreviations (SyntaxDefinition).Gravatar Hugo Herbelin2016-06-16
| |
* | Fixing printing of Polymorphic/Monomorphic.Gravatar Hugo Herbelin2016-06-16
| |
* | Fixing printing of Arguments.Gravatar Hugo Herbelin2016-06-16
| |
* | Printing notations as parsed.Gravatar Hugo Herbelin2016-06-16
| |
* | So as to beautify to work, do not use notations in Inductive typesGravatar Hugo Herbelin2016-06-16
| | | | | | | | | | | | | | | | with a clause where, nor Notation, nor Fixpoints. Should be certainly improved at least for Inductive types and Fixpoints, depending on whether there is a "where" clause for instance.
* | Fixing missing substitution / printing cases of TacSelect.Gravatar Pierre-Marie Pédrot2016-06-16
| |
* | Fixing printing of keeping hyp on the fly.Gravatar Hugo Herbelin2016-06-16
| |
* | Fixing printing of inversion as.Gravatar Hugo Herbelin2016-06-16
| |
* | Fixing extra space in printing destruct/induction as.Gravatar Hugo Herbelin2016-06-16
| |
* | Fixing printing of induction/destruct as.Gravatar Hugo Herbelin2016-06-16
| |
* | Fixing printing of pat%constr.Gravatar Hugo Herbelin2016-06-16
| |
* | A stronger invariant on the syntax of TacAssert, what allows for aGravatar Hugo Herbelin2016-06-16
| | | | | | | | | | | | simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
* \ \ Merge remote-tracking branch 'github/pr/194' into trunkGravatar Maxime Dénès2016-06-16
|\ \ \
| | * | Remove the syntax changes introduced by this branch.Gravatar Pierre-Marie Pédrot2016-06-15
| | | | | | | | | | | | | | | | | | | | | | | | We decided to only export the API, so that an external plugin can provide this feature without having to merge it in current Coq trunk. This postpones the attribute implementation in vernacular commands after 8.6.
| | * | Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | The rational is that 1. further typing flags may be available in the future 2. it makes it easier to trace and document the argument
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\ \ \ \ | | |_|/ | |/| |
* | | | printing.mllib: remove some other .mli-only from a .mllibGravatar Pierre Letouzey2016-06-07
| | | |
| | * | Adding an only printing flag to notations.Gravatar Pierre-Marie Pédrot2016-06-07
| |/ / |/| |
| * | Fixing problems introduced in 8.5 with Ltac trace report. E.g.Gravatar Hugo Herbelin2016-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Tactic Notation "f" constr(x) := apply x. Ltac g x := f x. Goal False. g I. (* Was printing Top.Top#<>#1 *) idtac; f I. (* Was not properly locating error *) This is a "a minima" fix. This a different fix than in trunk, so the merge will have to take the trunk version.
* | | About printing of traces of failures while calling ltac code.Gravatar Hugo Herbelin2016-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | An Ltac trace printing mechanism was introduced in 8.4 which was inadvertedly modified by a series of commits such as 8e10368c3, 91f44f1da7a, ... It was also sometimes buggy, iirc, when entering ML tactics which themselves were calling ltac code. It got really bad in 8.5 as in: Tactic Notation "f" constr(x) := apply x. Ltac g x := f x. Goal False. idtac; f I. (* bad location reporting *) g I. (* was referring to tactic name "Top.Top#<>#1" *) which this commit fixes. I don't have a clear idea of what would be the best ltac tracing mechanism, but to avoid it to be broken without being noticed, I started to add some tests. Eventually, it might be worth that an Ltac expert brainstrom on it!
* | | Removing "rename" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
| | |
* | | Removing "exact" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
| | |
* | | Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
| | | | | | | | | | | | | | | | | | Note that this breaks the compatibility, in a beneficial way I believe. Tactics defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction on a local identifier anymore. They must use the "fresh" primitive instead.
* | | Removing "double induction" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
| | |
* | | Move ide serialization libraries from lib/ to ide/Gravatar Emilio Jesus Gallego Arias2016-06-02
| | | | | | | | | | | | | | | | | | | | | This makes the core free from particular protocol choices. It should help with the ppx serialization project and shrinks clib.cma a bit.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\| |
* | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
| * | Pfedit.get_current_context refinement (fix #4523)Gravatar Matthieu Sozeau2016-05-26
| | | | | | | | | | | | | | | | | | | | | Return the most appropriate evar_map for commands that can run on non-focused proofs (like Check, Show and debug printers) so that universes and existentials are printed correctly (they are global to the proof). The API is backwards compatible.
* | | Put the "cofix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
| | |
* | | Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 14:06:51 +0000