aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.ml
AgeCommit message (Collapse)Author
2017-05-04Warning removed.Pierre Courtieu
2017-05-04labelizing argumentsPierre Courtieu
2017-05-04Adding an option "Printing Unfocused".Pierre Courtieu
Off by default. + small refactoring of emacs hacks in printer.ml.
2017-04-27Remove some unused values and typesGaetan Gilbert
2017-04-12Merge PR#441: Port Toplevel to the Stm APIMaxime Dénès
2017-04-12[flags] Documentation and a minor tweak.Emilio Jesus Gallego Arias
Mostly documentation and making a couple of local flags, local.
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-21[pp] Prepare for serialization, remove opaque glue.Emilio Jesus Gallego Arias
We also remove flushing operations `msg_with`, now the flushing responsibility belong to the owner of the formatter.
2017-03-07Fixing Bug 5383 (Hyps Limit) + small refactoring.Pierre Courtieu
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Namegen primitives now apply on evar constrs.Pierre-Marie Pédrot
Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough.
2017-02-14Moving printing code from Evd to Termops.Pierre-Marie Pédrot
2017-02-14Introducing contexts parameterized by the inner term type.Pierre-Marie Pédrot
This allows the decoupling of the notions of context containing kernel terms and context containing tactic-level terms.
2017-02-14Evar-normalizing functions now act on EConstrs.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers related to printing.Pierre-Marie Pédrot
2017-02-14Ltac now uses evar-based constrs.Pierre-Marie Pédrot
2017-02-14Tactic_matching API using EConstr.Pierre-Marie Pédrot
2017-02-14Goal API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-05Do not print dependent evars by default (expensive)Matthieu Sozeau
The option can be turned on by the user though.
2016-10-24Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-20Refine printing of pending unification constraintsMatthieu Sozeau
It now prints evars with candidates as well if there are any.
2016-09-27Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-24Moving "move" in the new proof engine.Hugo Herbelin
2016-08-26CLEANUP: adding "Context.Compacted.Declaration.of_named_decl" function, ↵Matej Kosik
which can be useful in general, and then simplifying "Printer.pr_named_decl" function
2016-08-26CLEANUP: renaming "Printer.pr_var_decl" function to "Printer.pr_named_decl"Matej Kosik
2016-08-26CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"Matej Kosik
2016-08-25CLEANUP: changing the definition of the "Context.NamedList.Declaration" typeMatej Kosik
2016-08-24CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionMatej Kosik
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Pierre Letouzey
module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
2016-06-19Add [Unset Printing Dependent Evars Line]Jason Gross
This allows a work-around for bug #4819, https://coq.inria.fr/bugs/show_bug.cgi?id=4819.
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-16proof mode: print unification constraintsMatthieu Sozeau
along with goals, with nice formatting.
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
2016-05-26Pfedit.get_current_context refinement (fix #4523)Matthieu Sozeau
Return the most appropriate evar_map for commands that can run on non-focused proofs (like Check, Show and debug printers) so that universes and existentials are printed correctly (they are global to the proof). The API is backwards compatible.
2016-05-16Put the "cofix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "fix" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "clear" tactic into the monad.Pierre-Marie Pédrot
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-03Remove extraneous space in coqtop/pg output (bug #4675).Guillaume Melquiond
2016-04-04Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into ↵Matthieu Sozeau
aspiwack-linear-comparison Fixing a -1 -> +1 typo
2016-03-30Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-25Univs: fix get_current_context (bug #4603, part I)Matthieu Sozeau
Return an evar_map with the right universes, when there are no focused subgoals or the proof is finished.
2016-03-20Moving Refine to its proper module.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
The current solution may not be totally ideal though. We generate names for anonymous evars on the fly at printing time, based on the Evar_kind data they are wearing. This means in particular that the printed name of an anonymous evar may change in the future because some unrelate evar has been solved or introduced.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-29 17:31:36 +0000