index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
printing
/
printer.mli
Age
Commit message (
Expand
)
Author
2017-06-16
Add printing of cumulativity in inductive types
Amin Timany
2017-06-16
Using UInfoInd for universes in inductive types
Amin Timany
2017-06-01
[emacs] [toplevel] Make emacs flag local to the toplevel.
Emilio Jesus Gallego Arias
2017-05-17
Merge PR#457: Adding an even more compact goal hyps mode.
Maxime Dénès
2017-05-04
Adding an option "Printing Unfocused".
Pierre Courtieu
2017-05-03
Adding an even more compact mode for goal display.
Pierre Courtieu
2017-02-14
Removing compatibility layers related to printing.
Pierre-Marie Pédrot
2017-02-14
Ltac now uses evar-based constrs.
Pierre-Marie Pédrot
2016-08-26
CLEANUP: renaming "Printer.pr_var_decl" function to "Printer.pr_named_decl"
Matej Kosik
2016-08-26
CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"
Matej Kosik
2016-06-16
Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.
Pierre-Marie Pédrot
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2016-01-11
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2015-11-02
Adding syntax "Show id" to show goal named id (shelved or not).
Hugo Herbelin
2015-10-28
Univs: local names handling.
Matthieu Sozeau
2015-10-28
Printing of @{} instances for polymorphic references in Print and About.
Matthieu Sozeau
2015-06-29
Assumptions: more informative print for False axiom (Close: #4054)
Enrico Tassi
2015-03-31
Generalisation of the "end command" argument of the goal printer.
Arnaud Spiwack
2015-01-24
Isolate a function for printing evar sets.
Hugo Herbelin
2015-01-17
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-12
Update headers.
Maxime Dénès
2014-12-04
Improving error message when one instance-hole is not found.
Hugo Herbelin
2014-11-20
Moving mutual inductive printing from Printer to Printmod.
Pierre-Marie Pédrot
2014-11-19
Print [uconstr] in genargs.
Arnaud Spiwack
2014-11-19
Printing function for [uconstr].
Arnaud Spiwack
2014-10-17
Experimental printing of the signature of open evars in Check.
Hugo Herbelin
2014-09-12
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-01
Coqide prints succesive hyps of the same type on 1 line
Pierre Boutillier
2014-07-11
Feedback: LoadedFile + Goals
Enrico Tassi
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-03-05
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2013-11-02
Adds a shelve tactic.
aspiwack
2013-09-18
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-03
Partly replacing list-based access functions in Evd. This is still
ppedrot
2013-05-14
Removing useless uses of Gmap.
ppedrot
2013-04-29
Merging Context and Sign.
ppedrot
2013-04-29
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-17
Improving error message in explain_cannot_find_well_typed_abstraction:
herbelin
2013-03-21
Robust display of NotConvertibleTypeField errors (fix #3008, #2995)
letouzey
2013-02-17
Added propagation of evars unification failure reasons for better
herbelin
2012-12-14
Modulification of identifier
ppedrot
2012-11-21
Print univ constraints generated by a constant or inductive (when flag is set)
barras
2012-08-08
Updating headers.
herbelin
2012-07-11
A friendlier printing of remaining goals when no goal is focused.
aspiwack
2012-07-04
Change how the number of open goals is printed.
aspiwack
2012-05-29
place all pretty-printing files in new dir printing/
letouzey
