aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/top_printers.ml
Commit message (Collapse)AuthorAge
...
| * Fixing #use"include" after vernac is added and ltac is moved to a plugin.Gravatar Hugo Herbelin2017-02-23
| |
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\|
* | Moving printing code from Evd to Termops.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
| |
| * Adding a printer for Proof.proof reflecting the focusing layout.Gravatar Hugo Herbelin2017-01-26
| | | | | | | | | | | | | | | | This is a modest contribution serving before all the purpose of displaying the focus stack and the shelf and give_up list. It does not print the sigma (while it could). Any improvements are welcome.
* | Introducing a new EConstr.t type to perform the nf_evar operation on demand.Gravatar Pierre-Marie Pédrot2016-11-08
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\
| * Remove no longer exported debug printerGravatar Matthieu Sozeau2016-10-21
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-08
|\|
| * Adding debugging printer for Genarg.ArgT.t.Gravatar Hugo Herbelin2016-10-08
| |
* | Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
|/ | | | | | There was no reason to keep them separate since quite a long time. Historically, they were making Genarg depend or not on upper strata of the code, but since it was moved to lib/ this is not justified anymore.
* Fixing extra returns in top_printers.ml (msg_notice not same semantics as pp).Gravatar Hugo Herbelin2016-07-19
|
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
| | | | For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
* 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
* 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.
* | Removing the Entry module now that rules need not be marshalled.Gravatar Pierre-Marie Pédrot2016-05-10
| |
* | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
| |
* | Fixing printing of toplevel values.Gravatar Pierre-Marie Pédrot2016-04-08
| | | | | | | | | | | | | | This is not perfect yet, in particular the whole precedence system is a real mess, as there is a real need for tidying up the Pptactic implementation. Nonetheless, printing toplevel values is only used for debugging purposes, where an ugly display is better than none at all.
* | Do not export entry_key from Pcoq anymore.Gravatar Pierre-Marie Pédrot2016-03-19
| |
* | Simplifying the code of Entry.Gravatar Pierre-Marie Pédrot2016-03-19
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Removing constr generic argument.Gravatar Pierre-Marie Pédrot2016-01-14
| |
* | Simplification of grammar_prod_item type.Gravatar Pierre-Marie Pédrot2016-01-02
| | | | | | | | Actually the identifier was never used and just carried along.
* | Finer-grained types for toplevel values.Gravatar Pierre-Marie Pédrot2015-12-21
| |
* | Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
| |
* | Tying the loop in tactic printing API.Gravatar Pierre-Marie Pédrot2015-12-18
| |
* | Type-safe Egramml.grammar_prod_item.Gravatar Pierre-Marie Pédrot2015-10-27
| |
* | Pcoq entries are given a proper module.Gravatar Pierre-Marie Pédrot2015-10-26
| | | | | | | | | | | | | | | | | | | | | | Entries defined in the Pcoq AST of symbols must be marshallable, because they are present in the libstack. Yet, CAMLP4/5 entries are not marshallable as they contain functional values. This is why the Pcoq module used a pair [string * string] to describe entries. It is obviously type-unsafe, so we define a new abstract type in its own module. There is a little issue though, which is that our entries and CAMLP4/5 entries must be kept synchronized through an association table. The Pcoq module tries to maintain this invariant.
| * Reverting modifications in dev/top_printers pushed mistakenly.Gravatar Pierre-Marie Pédrot2015-10-14
| |
| * Fixing perfomance issue of auto hints induced by universes.Gravatar Pierre-Marie Pédrot2015-10-14
| | | | | | | | | | | | | | Instead of brutally merging the whole evarmap coming from the clenv, we remember the context associated to the hint and we only merge that tiny part of constraints. We need to be careful for polymorphic hints though, as we have to refresh them beforehand.
* | Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
| | | | | | | | | | 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity.
* | Better debug printers for module paths.Gravatar Maxime Dénès2015-09-20
|/ | | | | | | | Now distinguishes between bound modules (Top#X) and submodules (Top.X). Could be useful for the regular printer as well (e.g. in error messages), but I don't know what the compatibility constraints are, so leaving it as it is for now.
* A printer for printing constants of the env (maybe useful when there are not ↵Gravatar Hugo Herbelin2015-07-30
| | | | too many of them).
* Adding a possible DEPRECATED flag to VERNAC EXTEND statements.Gravatar Pierre-Marie Pédrot2015-02-19
|
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
|
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
| | | | printing functions touched in the kernel).
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Compatibility ocaml 3.12.Gravatar Hugo Herbelin2014-12-30
|
* More printers for ltac signatures.Gravatar Hugo Herbelin2014-12-16
|
* Reactivating option "Set Printing Existential Instances" for asking printing ↵Gravatar Hugo Herbelin2014-12-04
| | | | full instances.
* Adding printers for ppproofview.Gravatar Hugo Herbelin2014-10-13
|
* Add debug printers for projections, fix printing of evar constraintsGravatar Matthieu Sozeau2014-10-10
| | | | and unsatisfiable constraints which were not done in the right environment.
* Adding printer for named_context_val and Goal.goal in debugger.Gravatar Hugo Herbelin2014-10-09
|
* Adding a printer for hints.Gravatar Hugo Herbelin2014-10-07
|
* Fixing interpretation of constr under binders which was broken afterGravatar Hugo Herbelin2014-10-02
| | | | | it became possible to have binding names themselves bound to ltac variables (2fcc458af16b).
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
| | | | | | | | so as to reproduce correctly the reduction behavior of existing projections, i.e. delta + iota. Make [projection] an abstract datatype in Names.ml, most of the patch is about using that abstraction. Fix unification.ml which tried canonical projections too early in presence of primitive projections.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 05:40:16 +0000