aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Collapse)Author
2015-08-15Revert the four previous commits and update the description of Richpp.Pierre-Marie Pédrot
Correcting the code w.r.t. to the API was not the right solution. Instead, the API comment had to be corrected.
2015-08-15More invariants in Richpp.Pierre-Marie Pédrot
We ensure statically by typing that the tags used by the rich printer are integers. Furthermore, we also expose through typing that tags are irrelevants in the returned XML.
2015-08-15More parametric type for generalized XML.Pierre-Marie Pédrot
2015-08-14Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Jason Gross
This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change in the semantics of arguments scopes: scopes can no longer be bound to Funclass or Sortclass (this does not seem to be useful)). It is useful to have function_scope for, e.g., function composition. This allows users to, e.g., automatically interpret ∘ as morphism composition when expecting a morphism of categories, as functor composition when expecting a functor, and as function composition when expecting a function. Additionally, it is nicer to have fewer special cases in the OCaml code, and give more things a uniform syntax. (The scope type_scope should not be special-cased; this change is coming up next.) Also explicitly define [function_scope] in theories/Init/Notations.v. This closes bug #3080, Build a [function_scope] like [type_scope], or allow [Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass] We now mention Funclass and Sortclass in the documentation of [Bind Scope] again.
2015-07-27Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-27Fixing bug #2169:Pierre-Marie Pédrot
"Print Module command shows module type expression incorrectly".
2015-07-18Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-09Fixing printing of primitive coinductive record status.Pierre-Marie Pédrot
They do not have eta-rule indeed, even though it was displayed as such.
2015-07-02Merge branch 'v8.5' into trunkMaxime Dénès
2015-06-29Assumptions: more informative print for False axiom (Close: #4054)Enrico Tassi
When an axiom of an empty type is matched in order to inhabit a type, do print that type (as if each use of that axiom was a distinct foo_subproof). E.g. Lemma w : True. Proof. case demon. Qed. Lemma x y : y = 0 /\ True /\ forall w, w = y. Proof. split. case demon. split; [ exact w | case demon ]. Qed. Print Assumptions x. Prints: Axioms: demon : False used in x to prove: forall w : nat, w = y used in w to prove: True used in x to prove: y = 0
2015-06-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
2015-06-25Remove other types not carried by interpretations in `Tacexpr`.Arnaud Spiwack
2015-06-25Remove useless `and_short_name` in interpreted level in `Tacexpr`.Arnaud Spiwack
2015-06-25Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
This allows fatal_error to be used for printing anomalies at loading time.
2015-06-24Make inductives that were assumed positive appear in `Print Assumptions`.Arnaud Spiwack
They appear as axioms of the form `Foo is positive`.
2015-06-24Add corresponding field in `VernacInductive`.Arnaud Spiwack
Makes sure not to generate inductive schemes of assumed positive types.
2015-06-24Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-24Add a space in cast since cast binds loosely.Gregory Malecha
Fixes bug 3936 This closes #73
2015-06-23Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
This allows fatal_error to be used for printing anomalies at loading time.
2015-06-22Merge remote-tracking branch 'forge/v8.5'Pierre Boutillier
2015-06-19Make end-of-proof output consistent across toplevels.Guillaume Melquiond
Ideally, the code should be shared between the various toplevels, but this is a lot more work than just fixing a few strings.
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-05-04Add a [Redirect] vernacular commandClément Pit--Claudel
The command [Redirect "filename" (...)] redirects all the output of [(...)] to file "filename.out". This is useful for storing the results of an [Eval compute], for redirecting the results of a large search, for automatically generating traces of interesting developments, and so on.
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure.
2015-04-09Merge branch 'v8.5' into trunkPierre Letouzey
2015-03-31Declarative mode: plug the specialised printers back.Arnaud Spiwack
It will not work in CoqIDE though, which handles printing its own way. It's a general remark that we have many ways of printing things in Coq and we should look for a unified structured framework to be shared between interfaces.
2015-03-31Better formatting of messages in proofs.Arnaud Spiwack
2015-03-31Generalisation of the "end command" argument of the goal printer.Arnaud Spiwack
This is meant to help integrate the printers of the declarative mode.
2015-03-30Merge branch 'v8.5' into trunkEnrico Tassi
2015-03-27Putting the From parameter of the Require command into the AST.Pierre-Marie Pédrot
2015-03-13rewiring Czar printers that were disabledPierre Corbineau
Backported from trunk.
2015-03-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-09Do not display the status of monomorphic constants unless in ↵Guillaume Melquiond
universe-polymorphism mode.
2015-03-02rewiring Czar printers that were disabledPierre Corbineau
2015-02-23Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-21Better English for #4070 implicit arguments message (thanks to Jason for his ↵Hugo Herbelin
help).
2015-02-20An answer to #4070 (message for implicit arguments of inl not clear).Hugo Herbelin
2015-02-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
Of course such proofs cannot be processed asynchronously
2015-02-10Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-06More efficient Richpp.Pierre-Marie Pédrot
We build the rich XML at once without generating the printed string.
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-25Merge branch 'v8.5' into trunk.Pierre-Marie Pédrot
2015-01-24Isolate a function for printing evar sets.Hugo Herbelin
2015-01-23Splitting ML tactics in one function per grammar entry.Pierre-Marie Pédrot
Furthermore, ML tactic dispatch is not done according to the type of its argument anymore.
2015-01-21Embedding the index of the ML tactic entry in the Tacexpr AST.Pierre-Marie Pédrot
This will allow to get rid of the fragile mechanism of discriminating which entry to call depending on the dynamic type of its arguments.
2015-01-18Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
printing functions touched in the kernel).
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
printing functions touched in the kernel).
2015-01-13Fix issue in printing due to de Bruijn bug when constructing compatibilityMatthieu Sozeau
constr for primitive records (not used anywhere else than printing). Problem reported by P. LeFanu Lumsdaine on HoTT/HoTT. Also add some minor fixes in detyping and pretty printing related to universes.
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-06 19:06:19 +0000