aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Collapse)AuthorAge
* Improving error message when one instance-hole is not found.Gravatar Hugo Herbelin2014-12-04
| | | | | | | | Still to do: - Decide between using SeveralInstancesFound or raising an error when multiple instances exist. - Use a proper printer for evars instead of the debugging pr_evar_map_filter printer in pr_constraints.
* Fixing printing of dirpathes in Ppconstr. It was reversed.Gravatar Pierre-Marie Pédrot2014-11-30
|
* Adding tag output to references in Ppconstr.Gravatar Pierre-Marie Pédrot2014-11-25
|
* Plugging console highlighting in for toplevel and compilation error messages.Gravatar Pierre-Marie Pédrot2014-11-24
|
* Removing useless flag of the historical move tactic.Gravatar Pierre-Marie Pédrot2014-11-22
|
* Setting printing flags on the printing of mutual inductives.Gravatar Pierre-Marie Pédrot2014-11-20
|
* Moving mutual inductive printing from Printer to Printmod.Gravatar Pierre-Marie Pédrot2014-11-20
|
* Print [uconstr] in genargs.Gravatar Arnaud Spiwack2014-11-19
|
* Proper printer for [uconstr] in [Pptactic].Gravatar Arnaud Spiwack2014-11-19
| | | | This particular instance is probably never called though.
* Printing function for [uconstr].Gravatar Arnaud Spiwack2014-11-19
| | | | The core is a "detyping" function for [closed_glob_constr]. Which interpretes the variable names according to the Ltac context, and apply the standard detyping procedure to typed terms in the closure.
* Adding rich-printing facilities to Printmod.Gravatar Pierre-Marie Pédrot2014-11-19
|
* Adding notation terminals to coqtop highlight.Gravatar Pierre-Marie Pédrot2014-11-17
|
* Fixing semantics of Ppconstr.print_hunks.Gravatar Pierre-Marie Pédrot2014-11-17
|
* Missing keywords in Ppconstr.Gravatar Pierre-Marie Pédrot2014-11-17
|
* Setting printing tags for Ltac.Gravatar Pierre-Marie Pédrot2014-11-17
|
* Moving printing code for red_expr and may_eval to Pptactic.Gravatar Pierre-Marie Pédrot2014-11-17
|
* Default styles for printing tags.Gravatar Pierre-Marie Pédrot2014-11-17
| | | | They should be rather sensible, but de gustibus & coloribus...
* Setting error tag on generic errors returned by Coqtop.Gravatar Pierre-Marie Pédrot2014-11-17
|
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | reference" and "simpl pattern" in the code (maybe we should have merged them instead, but I finally decided to enforce their difference, even if some compatibility is to be preversed - the idea is that at some time "simpl reference" would only call a weak-head simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n) rather than S(S(n)) which could be useful for better using induction hypotheses. In the process we also implement the following: - 'simpl "+"' is accepted to reduce all applicative subterms whose head symbol is written "+" (in the toplevel scope); idem for vm_compute and native_compute - 'simpl reference' works even if reference has maximally inserted implicit arguments (this solves the "simpl fst" incompatibility) - compatibility of ltac expressions referring to vm_compute and native_compute with functor application should now work (i.e. vm_compute and native_compute are now taken into account in tacsubst.ml) - for compatibility, "simpl eq" (assuming no maximal implicit args in eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed. By the way, is "mul" on nat defined optimally? "3*n" simplifies to "n+(n+(n+0))". Are there some advantages of this compared to have it simplified to "n+n+n" (i.e. to "(n+n)+n").
* Adding tags to messages.Gravatar Pierre-Marie Pédrot2014-11-15
|
* Additional style tags for constrs.Gravatar Pierre-Marie Pédrot2014-11-15
|
* Setting a keyword tag in Ppconstr.Gravatar Pierre-Marie Pédrot2014-11-15
|
* Adding a pretty-printing style library.Gravatar Pierre-Marie Pédrot2014-11-15
|
* Move conjugate_verb_to_be next to cString.plural.Gravatar Hugo Herbelin2014-11-13
|
* Plug the dynamic tags in the Richpp mechanism.Gravatar Pierre-Marie Pédrot2014-11-10
|
* Removing a unused boolean in the TacMove node of tacexpr AST.Gravatar Pierre-Marie Pédrot2014-11-09
|
* Removing the legacy intro tactic code.Gravatar Pierre-Marie Pédrot2014-11-07
|
* lib/RichPp: Rename into Richpp.Gravatar Yann Régis-Gianas2014-11-05
| | | | | | printing/RichPrinter: Rename into Richprinter. printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp. printing/Richprinter: Cosmetics.
* printing/Ppvernac: Fix missing keyword tagging on theorem introducers.Gravatar Yann Régis-Gianas2014-11-05
|
* printing/Ppvernac: Fix missing keyword tagging on definition introducers.Gravatar Yann Régis-Gianas2014-11-05
|
* printing/Ppvernac: Cosmetics.Gravatar Yann Régis-Gianas2014-11-05
|
* printing/Ppannotation: New annotation for tactic syntactic objects.Gravatar Regis-Gianas2014-11-04
| | | | | | printing/Pptactic: Tag tactics pretty-printing. printing/Ppvernac: Use the relevent Pptactic pretty-printer. printing/RichPrinter: Publish two new services.
* printing/Pptactic.Make: New.Gravatar Regis-Gianas2014-11-04
| | | | | | - Functorize with respect to the pretty-printer for constr. - Include the application of Make to Ppconstr at toplevel in order to preserve previous behavior.
* printing/Pptacticsig: New signature for tactic pretty-printers.Gravatar Regis-Gianas2014-11-04
| | | | printing/Pptactic: Use it.
* lib/Ppconstr: Cosmetics.Gravatar Regis-Gianas2014-11-04
|
* Rebase artefact.Gravatar Regis-Gianas2014-11-04
|
* lib/Pp.tag: New.Gravatar Regis-Gianas2014-11-04
| | | | | A combinator to introduce tags. printing/{Ppconstr, Ppvernac}: Use it.
* printing/Ppannotation: Introduce a new annotation for keywords.Gravatar Regis-Gianas2014-11-04
| | | | printing/{Ppconstr, Ppvernac}: Use it.
* printing/richPrinter: Fix incorrect signatures.Gravatar Regis-Gianas2014-11-04
|
* printing/RichPrinter: New API for rich pretty-printing.Gravatar Regis-Gianas2014-11-04
| | | | | printing/Ppannotation: Define the projection of annotations into XML attributes. lib/richPp: Implements valid entities escaping.
* Ppvernac: Publish new rich pretty-printer.Gravatar Regis-Gianas2014-11-04
| | | | Ppconstr: Fix a typo in comments.
* Ppannotation.t: New constructor AVernac.Gravatar Regis-Gianas2014-11-04
| | | | Ppvernac.RichPp: New rich pretty-printer.
* Ppvernacsig: New.Gravatar Regis-Gianas2014-11-04
| | | | | | - Define the signature for a pretty-printer of vernacular commands. Ppvernac: Use it.
* Ppvernac.Make: NewGravatar Regis-Gianas2014-11-04
| | | | | | | | - Ppvernac is now functorized with respect to a Ppconstr printer. - Preserve previous behavior by instantiating this functor with Ppconstr.
* Ppvernac: Cosmetics.Gravatar Regis-Gianas2014-11-04
|
* Ppannotation: New.Gravatar Regis-Gianas2014-11-04
| | | | | | | | | Define the annotations stored in semi-structured pretty-prints. Ppconstrsig: New. Contains the signature of a pretty-printer for ppconstr. Ppconstr: Export a new rich pretty-printer for constr_expr and co.
* printing/Ppconstr.Make:Gravatar Regis-Gianas2014-11-04
| | | | | | | | | | - Functorize Ppconstr with respect to a set of tagging functions. - These functions are meant to introduce tags to produce semistructured pretty printings. printing/Ppconstr: Preserve the previous behaviour of this module by instantiating Make with tagging functions that do nothing.
* printing/Ppconstr.print_hunks:Gravatar Regis-Gianas2014-11-04
| | | | | Make evaluation order explicit. (Do not rely anymore on ocaml evaluation order, which is unspecified.)
* printing/Ppconstr: Cosmetics.Gravatar Regis-Gianas2014-11-04
|
* Removing the old rename tactic.Gravatar Pierre-Marie Pédrot2014-11-04
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 20:24:35 +0000