aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printer.mli
Commit message (Expand)AuthorAge
* Merge PR#457: Adding an even more compact goal hyps mode.Gravatar Maxime Dénès2017-05-17
|\
* | Adding an option "Printing Unfocused".Gravatar Pierre Courtieu2017-05-04
| * Adding an even more compact mode for goal display.Gravatar Pierre Courtieu2017-05-03
|/
* Removing compatibility layers related to printing.Gravatar Pierre-Marie Pédrot2017-02-14
* Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* CLEANUP: renaming "Printer.pr_var_decl" function to "Printer.pr_named_decl"Gravatar Matej Kosik2016-08-26
* CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"Gravatar Matej Kosik2016-08-26
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
* \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\ \
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
|/ /
* | Adding syntax "Show id" to show goal named id (shelved or not).Gravatar Hugo Herbelin2015-11-02
* | Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* | Printing of @{} instances for polymorphic references in Print and About.Gravatar Matthieu Sozeau2015-10-28
* | Assumptions: more informative print for False axiom (Close: #4054)Gravatar Enrico Tassi2015-06-29
|/
* Generalisation of the "end command" argument of the goal printer.Gravatar Arnaud Spiwack2015-03-31
* Isolate a function for printing evar sets.Gravatar Hugo Herbelin2015-01-24
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* Improving error message when one instance-hole is not found.Gravatar Hugo Herbelin2014-12-04
* Moving mutual inductive printing from Printer to Printmod.Gravatar Pierre-Marie Pédrot2014-11-20
* Print [uconstr] in genargs.Gravatar Arnaud Spiwack2014-11-19
* Printing function for [uconstr].Gravatar Arnaud Spiwack2014-11-19
* Experimental printing of the signature of open evars in Check.Gravatar Hugo Herbelin2014-10-17
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Coqide prints succesive hyps of the same type on 1 lineGravatar Pierre Boutillier2014-09-01
* Feedback: LoadedFile + GoalsGravatar Enrico Tassi2014-07-11
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Adds a shelve tactic.Gravatar aspiwack2013-11-02
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Partly replacing list-based access functions in Evd. This is stillGravatar ppedrot2013-09-03
* Removing useless uses of Gmap.Gravatar ppedrot2013-05-14
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Improving error message in explain_cannot_find_well_typed_abstraction:Gravatar herbelin2013-04-17
* Robust display of NotConvertibleTypeField errors (fix #3008, #2995)Gravatar letouzey2013-03-21
* Added propagation of evars unification failure reasons for betterGravatar herbelin2013-02-17
* Modulification of identifierGravatar ppedrot2012-12-14
* Print univ constraints generated by a constant or inductive (when flag is set)Gravatar barras2012-11-21
* Updating headers.Gravatar herbelin2012-08-08
* A friendlier printing of remaining goals when no goal is focused.Gravatar aspiwack2012-07-11
* Change how the number of open goals is printed.Gravatar aspiwack2012-07-04
* place all pretty-printing files in new dir printing/Gravatar letouzey2012-05-29