aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Collapse)AuthorAge
...
* Term: include a function to print termsGravatar Enrico Tassi2014-12-26
| | | | | | I find it very odd not to have a pretty printer for terms than can be called from *everywhere*. This commit sticks in Term a long spaghetti to let Printer install a printing function.
* A global [gfail] tactic which works like [fail] except that it fails even if ↵Gravatar Arnaud Spiwack2014-12-23
| | | | | | there is no focused goal. The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not.
* Fix compilation error in some configurations.Gravatar Arnaud Spiwack2014-12-23
| | | | | | This was due to the unqualified uses of "Lazy" being disambiguated in different manners. I just changed the constructor name to "Select". Fixes #3877.
* Add a backtracking version of Ltac's [match].Gravatar Arnaud Spiwack2014-12-19
| | | | [multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well.
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
|
* Fixed bad newlines in output for std output and emacs.Gravatar Pierre Courtieu2014-12-18
| | | | | I added a emacs_logger. Still need to cleanup std_logger.
* msg_info now puts infomsg tag in emacs mode.Gravatar Pierre Courtieu2014-12-16
| | | | | Fixes the idtac "string" not appearing in proofgeneral because printined *before* the goal.
* Changed bullet informations to warning for better display in PG.Gravatar Pierre Courtieu2014-12-15
| | | | | Since it displays together with the goal, it is better (for pg and other interfaces probably) that they are in a different message.
* About now accepts hypothesis names and goal selector.Gravatar Pierre Courtieu2014-12-15
|
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
| | | | [tryif t then t2 else t3] behaves like [t;t2] if [t] has at least one success, or [t3] otherwise. It generalises [t||t3] as failures from [t2] will not be caught.
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
| | | | You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
| | | | Documentation also updated.
* 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 02:42:49 +0000