aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printer.ml
Commit message (Collapse)AuthorAge
...
| | * Adding an even more compact mode for goal display.Gravatar Pierre Courtieu2017-05-03
| |/ | | | | | | | | | | | | | | | | | | | | We want to print variables in vertical boxes as much as possible. The criterion to distinguish "variable" from "hypothesis" is not obvious. We chose this one but may change it in the future: X:T is a variable if T is not of type Prop AND T is "simple" which means T is either id or (t T1 .. Tn) Ti's are sort-typed (typicall Ti:Type, but not Ti:nat).
| * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| |
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/ | | | Now it is a private field, locations are optional.
* Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\
| * [flags] Documentation and a minor tweak.Gravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | | | | Mostly documentation and making a couple of local flags, local.
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\|
| * [pp] Prepare for serialization, remove opaque glue.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | We also remove flushing operations `msg_with`, now the flushing responsibility belong to the owner of the formatter.
| * Fixing Bug 5383 (Hyps Limit) + small refactoring.Gravatar Pierre Courtieu2017-03-07
| |
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\|
* | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | 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.
* | Moving printing code from Evd to Termops.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | This allows the decoupling of the notions of context containing kernel terms and context containing tactic-level terms.
* | Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | 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
| |
* | Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Goal API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/|
| * Do not print dependent evars by default (expensive)Gravatar Matthieu Sozeau2016-11-05
| | | | | | | | The option can be turned on by the user though.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\|
| * Refine printing of pending unification constraintsGravatar Matthieu Sozeau2016-10-20
| | | | | | | | It now prints evars with candidates as well if there are any.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-27
|\|
| * Moving "move" in the new proof engine.Gravatar Hugo Herbelin2016-09-24
| |
* | CLEANUP: adding "Context.Compacted.Declaration.of_named_decl" function, ↵Gravatar Matej Kosik2016-08-26
| | | | | | | | which can be useful in general, and then simplifying "Printer.pr_named_decl" function
* | 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
| |
* | CLEANUP: changing the definition of the "Context.NamedList.Declaration" typeGravatar Matej Kosik2016-08-25
| |
* | CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-24
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* Add [Unset Printing Dependent Evars Line]Gravatar Jason Gross2016-06-19
| | | | | This allows a work-around for bug #4819, https://coq.inria.fr/bugs/show_bug.cgi?id=4819.
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
|
* proof mode: print unification constraintsGravatar Matthieu Sozeau2016-06-16
| | | | along with goals, with nice formatting.
* 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-06-01
|\ \
* | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | Pfedit.get_current_context refinement (fix #4523)Gravatar Matthieu Sozeau2016-05-26
| | | | | | | | | | | | | | | | | | | | | 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.
* | | Put the "cofix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
| | |
* | | Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
| | |
* | | Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\| |
| * | Remove extraneous space in coqtop/pg output (bug #4675).Gravatar Guillaume Melquiond2016-05-03
| | |
* | | Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into ↵Gravatar Matthieu Sozeau2016-04-04
|\ \ \ | | | | | | | | | | | | | | | | | | | | aspiwack-linear-comparison Fixing a -1 -> +1 typo
* \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\ \ \ \ | | |/ / | |/| |
| * | | Univs: fix get_current_context (bug #4603, part I)Gravatar Matthieu Sozeau2016-03-25
| | | | | | | | | | | | | | | | | | | | Return an evar_map with the right universes, when there are no focused subgoals or the proof is finished.
* | | | Moving Refine to its proper module.Gravatar Pierre-Marie Pédrot2016-03-20
| | | |
* | | | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \ \ \
* \ \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|\ \ \ \ \ | | |/ / / | |/| | |
| * | | | Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Originally, rel-context was represented as: Context.rel_context = Names.Name.t * Constr.t option * Constr.t Now it is represented as: Context.Rel.t = LocalAssum of Names.Name.t * Constr.t | LocalDef of Names.Name.t * Constr.t * Constr.t Originally, named-context was represented as: Context.named_context = Names.Id.t * Constr.t option * Constr.t Now it is represented as: Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t Motivation: (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction" function which looked like this: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 04:31:45 +0000