index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
printing
Commit message (
Expand
)
Author
Age
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
correct some ends of .mllib files (avoid a broken tolink.ml)
letouzey
2012-08-24
*
Added support for option Local (at module level) in Tactic Notation.
herbelin
2012-08-11
*
Updating headers.
herbelin
2012-08-08
*
Avoid Pp.std_ppcmds in Misctypes.sort_info
letouzey
2012-08-07
*
Bigint: avoid dependency over Pp
letouzey
2012-07-30
*
Slight modification to the printing of goals when in emacs mode.
courtieu
2012-07-21
*
Fixing test-suite
pboutill
2012-07-20
*
Getting rid of the undocumented [complete] tactic, which was
ppedrot
2012-07-19
*
A friendlier printing of remaining goals when no goal is focused.
aspiwack
2012-07-11
*
Fixing Print Assumption display
ppedrot
2012-07-10
*
Small change in the printing of proofs for use by coqide.
aspiwack
2012-07-10
*
Another correction to the dependent existential variable printing
aspiwack
2012-07-10
*
The tactic remember now accepts a final eqn:H option (grant wish #2489)
letouzey
2012-07-09
*
induction/destruct : nicer syntax for generating equations (solves #2741)
letouzey
2012-07-09
*
Avoid a warning about unprintable new command Print Namespace
letouzey
2012-07-09
*
Notation: a new annotation "compat 8.x" extending "only parsing"
letouzey
2012-07-05
*
Fixes a bug in Ppvernac which had braces and bullets printed with an ending
aspiwack
2012-07-04
*
Change how the number of open goals is printed.
aspiwack
2012-07-04
*
When focused on an empty list of goal (after finishing a subproof introduced
aspiwack
2012-07-04
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Fixing bug #2809 (anomaly when printing a module with notations due to
herbelin
2012-06-20
*
Fixing some inconsistencies of constr printer wrt constr parser
herbelin
2012-06-19
*
Internalization of pattern is done in two phases.
pboutill
2012-06-14
*
Fixing test-suite after last storm in Pp.
pboutill
2012-06-12
*
Replacing some str with strbrk
ppedrot
2012-06-04
*
More uniformisation in Pp.warn functions.
ppedrot
2012-05-30
*
remove many excessive open Util & Errors in mli's
letouzey
2012-05-29
*
place all pretty-printing files in new dir printing/
letouzey
2012-05-29