aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
2016-06-06Fixing problems introduced in 8.5 with Ltac trace report. E.g.Hugo Herbelin
2016-05-26Pfedit.get_current_context refinement (fix #4523)Matthieu Sozeau
2016-05-03Remove extraneous space in coqtop/pg output (bug #4675).Guillaume Melquiond
2016-04-19Revert "Fixing printing of surrounding parentheses in "ltac:"."Hugo Herbelin
2016-04-17Fixing printing of surrounding parentheses in "ltac:".Hugo Herbelin
2016-03-25Univs: fix get_current_context (bug #4603, part I)Matthieu Sozeau
2016-03-10Primitive projections: protect kernel from erroneous definitions.Matthieu Sozeau
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2016-01-23Implement support for universe binder lists in Instance and Program Fixpoint/...Matthieu Sozeau
2016-01-20Update copyright headers.Maxime Dénès
2015-12-03Improving over printing of let-tuple (see #4447).Hugo Herbelin
2015-12-02Dead code from August 2014 in apply in.Hugo Herbelin
2015-11-02Adding syntax "Show id" to show goal named id (shelved or not).Hugo Herbelin
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-28Printing of @{} instances for polymorphic references in Print and About.Matthieu Sozeau
2015-10-08Axioms now support the universe binding syntax.Pierre-Marie Pédrot
2015-10-08Goptions: new value type: optional stringEnrico Tassi
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-10-05Univs: fix printing bug #3797.Matthieu Sozeau
2015-09-20Print Assumptions shows engagement.Maxime Dénès
2015-09-14Univs: Add universe binding lists to definitionsMatthieu Sozeau
2015-08-15Revert the four previous commits and update the description of Richpp.Pierre-Marie Pédrot
2015-08-15More invariants in Richpp.Pierre-Marie Pédrot
2015-08-15More parametric type for generalized XML.Pierre-Marie Pédrot
2015-07-27Fixing bug #2169:Pierre-Marie Pédrot
2015-07-09Fixing printing of primitive coinductive record status.Pierre-Marie Pédrot
2015-06-29Assumptions: more informative print for False axiom (Close: #4054)Enrico Tassi
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
2015-06-25Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
2015-06-24Add a space in cast since cast binds loosely.Gregory Malecha
2015-06-19Make end-of-proof output consistent across toplevels.Guillaume Melquiond
2015-05-04Add a [Redirect] vernacular commandClément Pit--Claudel
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-03-31Declarative mode: plug the specialised printers back.Arnaud Spiwack
2015-03-31Better formatting of messages in proofs.Arnaud Spiwack
2015-03-31Generalisation of the "end command" argument of the goal printer.Arnaud Spiwack
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
2015-03-09Do not display the status of monomorphic constants unless in universe-polymor...Guillaume Melquiond
2015-02-21Better English for #4070 implicit arguments message (thanks to Jason for his ...Hugo Herbelin
2015-02-20An answer to #4070 (message for implicit arguments of inl not clear).Hugo Herbelin
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-02-06More efficient Richpp.Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-24Isolate a function for printing evar sets.Hugo Herbelin
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-13Fix issue in printing due to de Bruijn bug when constructing compatibilityMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
2015-01-08Continuing 785f82ee1 on reverting not only f5d7b2b1e but alsoHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 04:05:23 +0000