index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
printing
/
printer.mli
Commit message (
Expand
)
Author
Age
*
Generalisation of the "end command" argument of the goal printer.
Arnaud Spiwack
2015-03-31
*
Isolate a function for printing evar sets.
Hugo Herbelin
2015-01-24
*
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-17
*
Update headers.
Maxime Dénès
2015-01-12
*
Improving error message when one instance-hole is not found.
Hugo Herbelin
2014-12-04
*
Moving mutual inductive printing from Printer to Printmod.
Pierre-Marie Pédrot
2014-11-20
*
Print [uconstr] in genargs.
Arnaud Spiwack
2014-11-19
*
Printing function for [uconstr].
Arnaud Spiwack
2014-11-19
*
Experimental printing of the signature of open evars in Check.
Hugo Herbelin
2014-10-17
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
Coqide prints succesive hyps of the same type on 1 line
Pierre Boutillier
2014-09-01
*
Feedback: LoadedFile + Goals
Enrico Tassi
2014-07-11
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Adds a shelve tactic.
aspiwack
2013-11-02
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
Partly replacing list-based access functions in Evd. This is still
ppedrot
2013-09-03
*
Removing useless uses of Gmap.
ppedrot
2013-05-14
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Improving error message in explain_cannot_find_well_typed_abstraction:
herbelin
2013-04-17
*
Robust display of NotConvertibleTypeField errors (fix #3008, #2995)
letouzey
2013-03-21
*
Added propagation of evars unification failure reasons for better
herbelin
2013-02-17
*
Modulification of identifier
ppedrot
2012-12-14
*
Print univ constraints generated by a constant or inductive (when flag is set)
barras
2012-11-21
*
Updating headers.
herbelin
2012-08-08
*
A friendlier printing of remaining goals when no goal is focused.
aspiwack
2012-07-11
*
Change how the number of open goals is printed.
aspiwack
2012-07-04
*
place all pretty-printing files in new dir printing/
letouzey
2012-05-29