aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* correct some ends of .mllib files (avoid a broken tolink.ml)Gravatar letouzey2012-08-24
* Added support for option Local (at module level) in Tactic Notation.Gravatar herbelin2012-08-11
* Updating headers.Gravatar herbelin2012-08-08
* Avoid Pp.std_ppcmds in Misctypes.sort_infoGravatar letouzey2012-08-07
* Bigint: avoid dependency over PpGravatar letouzey2012-07-30
* Slight modification to the printing of goals when in emacs mode.Gravatar courtieu2012-07-21
* Fixing test-suiteGravatar pboutill2012-07-20
* Getting rid of the undocumented [complete] tactic, which wasGravatar ppedrot2012-07-19
* A friendlier printing of remaining goals when no goal is focused.Gravatar aspiwack2012-07-11
* Fixing Print Assumption displayGravatar ppedrot2012-07-10
* Small change in the printing of proofs for use by coqide.Gravatar aspiwack2012-07-10
* Another correction to the dependent existential variable printingGravatar aspiwack2012-07-10
* The tactic remember now accepts a final eqn:H option (grant wish #2489)Gravatar letouzey2012-07-09
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
* Avoid a warning about unprintable new command Print NamespaceGravatar letouzey2012-07-09
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
* Fixes a bug in Ppvernac which had braces and bullets printed with an endingGravatar aspiwack2012-07-04
* Change how the number of open goals is printed.Gravatar aspiwack2012-07-04
* When focused on an empty list of goal (after finishing a subproof introducedGravatar aspiwack2012-07-04
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Fixing bug #2809 (anomaly when printing a module with notations due toGravatar herbelin2012-06-20
* Fixing some inconsistencies of constr printer wrt constr parserGravatar herbelin2012-06-19
* Internalization of pattern is done in two phases.Gravatar pboutill2012-06-14
* Fixing test-suite after last storm in Pp.Gravatar pboutill2012-06-12
* Replacing some str with strbrkGravatar ppedrot2012-06-04
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* place all pretty-printing files in new dir printing/Gravatar letouzey2012-05-29