aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
2015-12-18CLEANUP: Vernacexpr.vernac_exprMatej Kosik
2015-12-18Tying the loop in tactic printing API.Pierre-Marie Pédrot
2015-12-17Getting rid of some hardwired generic arguments.Pierre-Marie Pédrot
2015-12-08Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-05Moving extended_rel_vect/extended_rel_list to the kernel.Hugo Herbelin
2015-12-04Getting rid of the dynamic node of the tactic AST.Pierre-Marie Pédrot
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
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-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-02Adding syntax "Show id" to show goal named id (shelved or not).Hugo Herbelin
2015-10-29Make the code of compare functions linear in the number of constructors.Arnaud Spiwack
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-28Printing of @{} instances for polymorphic references in Print and About.Matthieu Sozeau
2015-10-19Type delayed_open_constr is now monotonic.Pierre-Marie Pédrot
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
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-06Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-05Univs: fix printing bug #3797.Matthieu Sozeau
2015-09-25Show assumptions of well-foundedness in `Print Assumptions`Arnaud Spiwack
2015-09-25Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-25Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...Arnaud Spiwack
2015-09-20Print Assumptions shows engagement.Maxime Dénès
2015-09-17Merge branch 'v8.5' into trunkMaxime 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-08-14Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Jason Gross
2015-07-27Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-27Fixing bug #2169:Pierre-Marie Pédrot
2015-07-18Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-09Fixing printing of primitive coinductive record status.Pierre-Marie Pédrot
2015-07-02Merge branch 'v8.5' into trunkMaxime Dénès
2015-06-29Assumptions: more informative print for False axiom (Close: #4054)Enrico Tassi
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 02:22:28 +0000