aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
* Improving over printing of let-tuple (see #4447).Gravatar Hugo Herbelin2015-12-03
* Dead code from August 2014 in apply in.Gravatar Hugo Herbelin2015-12-02
* Adding syntax "Show id" to show goal named id (shelved or not).Gravatar Hugo Herbelin2015-11-02
* Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* Printing of @{} instances for polymorphic references in Print and About.Gravatar Matthieu Sozeau2015-10-28
* Axioms now support the universe binding syntax.Gravatar Pierre-Marie Pédrot2015-10-08
* Goptions: new value type: optional stringGravatar Enrico Tassi2015-10-08
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* Univs: fix printing bug #3797.Gravatar Matthieu Sozeau2015-10-05
* Print Assumptions shows engagement.Gravatar Maxime Dénès2015-09-20
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Revert the four previous commits and update the description of Richpp.Gravatar Pierre-Marie Pédrot2015-08-15
* More invariants in Richpp.Gravatar Pierre-Marie Pédrot2015-08-15
* More parametric type for generalized XML.Gravatar Pierre-Marie Pédrot2015-08-15
* Fixing bug #2169:Gravatar Pierre-Marie Pédrot2015-07-27
* Fixing printing of primitive coinductive record status.Gravatar Pierre-Marie Pédrot2015-07-09
* Assumptions: more informative print for False axiom (Close: #4054)Gravatar Enrico Tassi2015-06-29
* Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Gravatar Lionel Rieg2015-06-26
* Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-25
* Add a space in cast since cast binds loosely.Gravatar Gregory Malecha2015-06-24
* Make end-of-proof output consistent across toplevels.Gravatar Guillaume Melquiond2015-06-19
* Add a [Redirect] vernacular commandGravatar Clément Pit--Claudel2015-05-04
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Declarative mode: plug the specialised printers back.Gravatar Arnaud Spiwack2015-03-31
* Better formatting of messages in proofs.Gravatar Arnaud Spiwack2015-03-31
* Generalisation of the "end command" argument of the goal printer.Gravatar Arnaud Spiwack2015-03-31
* Putting the From parameter of the Require command into the AST.Gravatar Pierre-Marie Pédrot2015-03-27
* rewiring Czar printers that were disabledGravatar Pierre Corbineau2015-03-13
* Do not display the status of monomorphic constants unless in universe-polymor...Gravatar Guillaume Melquiond2015-03-09
* Better English for #4070 implicit arguments message (thanks to Jason for his ...Gravatar Hugo Herbelin2015-02-21
* An answer to #4070 (message for implicit arguments of inl not clear).Gravatar Hugo Herbelin2015-02-20
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* More efficient Richpp.Gravatar Pierre-Marie Pédrot2015-02-06
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Isolate a function for printing evar sets.Gravatar Hugo Herbelin2015-01-24
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Fix issue in printing due to de Bruijn bug when constructing compatibilityGravatar Matthieu Sozeau2015-01-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* Continuing 785f82ee1 on reverting not only f5d7b2b1e but alsoGravatar Hugo Herbelin2015-01-08
* Fixed and extend bullet related info/error messages. + doc.Gravatar Pierre Courtieu2015-01-08
* Revert "Term: include a function to print terms"Gravatar Enrico Tassi2014-12-27
* Term: include a function to print termsGravatar Enrico Tassi2014-12-26
* A global [gfail] tactic which works like [fail] except that it fails even if ...Gravatar Arnaud Spiwack2014-12-23
* Fix compilation error in some configurations.Gravatar Arnaud Spiwack2014-12-23
* Add a backtracking version of Ltac's [match].Gravatar Arnaud Spiwack2014-12-19
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
* Fixed bad newlines in output for std output and emacs.Gravatar Pierre Courtieu2014-12-18
* msg_info now puts infomsg tag in emacs mode.Gravatar Pierre Courtieu2014-12-16
* Changed bullet informations to warning for better display in PG.Gravatar Pierre Courtieu2014-12-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 19:03:14 +0000