aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Collapse)AuthorAge
* Addressing OCaml compilation warnings.Gravatar Hugo Herbelin2016-09-16
| | | | One of them revealed a true bug.
* Fix bug #4940: Tactic notation printing could be more informative.Gravatar Pierre-Marie Pédrot2016-09-09
|
* Fix tagging of notations.Gravatar Pierre-Marie Pédrot2016-08-29
| | | | We only tag the non-whitespace substrings, rather than the whole terminal token.
* Support qualified identifiers in Show Match (bug #5050).Gravatar Guillaume Melquiond2016-08-27
|
* Complementing previous commit on fixes for printing binding patterns.Gravatar Hugo Herbelin2016-07-19
|
* Some extra fixes in printing patterns in binders.Gravatar Hugo Herbelin2016-07-19
| | | | | | | | | | - typo in notation_ops.ml - factorization of patterns in ppconstr.ml - update of test-suite - printing of cast of a binding pattern if in mode "printing all" The question of whether or not to print the type of a binding pattern by default seems open to me.
* Taking into account binding patterns when agglutinating sequences of binders.Gravatar Hugo Herbelin2016-07-19
| | | | | Supporting accordingly printing of sequences of binders including binding patterns.
* 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.
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-28 05:29:35 +0000