aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
2015-09-25Show assumptions of well-foundedness in `Print Assumptions`Arnaud Spiwack
2015-09-25Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...Arnaud Spiwack
2015-06-24Make inductives that were assumed positive appear in `Print Assumptions`.Arnaud Spiwack
2015-06-24Add corresponding field in `VernacInductive`.Arnaud Spiwack
2015-06-24Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-24Add a space in cast since cast binds loosely.Gregory Malecha
2015-06-23Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote
2015-06-22Merge remote-tracking branch 'forge/v8.5'Pierre Boutillier
2015-06-19Make end-of-proof output consistent across toplevels.Guillaume Melquiond
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
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-04-09Merge branch 'v8.5' into trunkPierre Letouzey
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-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
2015-03-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-09Do not display the status of monomorphic constants unless in universe-polymor...Guillaume Melquiond
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
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
2015-02-10Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-06More efficient Richpp.Pierre-Marie Pédrot
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
2015-01-21Embedding the index of the ML tactic entry in the Tacexpr AST.Pierre-Marie Pédrot
2015-01-18Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
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
2015-01-08Fixed and extend bullet related info/error messages. + doc.Pierre Courtieu
2014-12-27Revert "Term: include a function to print terms"Enrico Tassi
2014-12-26Term: include a function to print termsEnrico Tassi
2014-12-23A global [gfail] tactic which works like [fail] except that it fails even if ...Arnaud Spiwack
2014-12-23Fix compilation error in some configurations.Arnaud Spiwack
2014-12-19Add a backtracking version of Ltac's [match].Arnaud Spiwack
2014-12-18Proof using: New vernacular to name sets of section variablesEnrico Tassi
2014-12-18Fixed bad newlines in output for std output and emacs.Pierre Courtieu
2014-12-16msg_info now puts infomsg tag in emacs mode.Pierre Courtieu
2014-12-15Changed bullet informations to warning for better display in PG.Pierre Courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 06:49:39 +0000