aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
2016-01-17Getting rid of the awkward unpack mechanism from Genarg.Pierre-Marie Pédrot
2016-01-17Temporary commit getting rid of Obj.magic unsafety for Genarg.Pierre-Marie Pédrot
2016-01-16Tactic notation printing accesses all the token data.Pierre-Marie Pédrot
2016-01-14Removing constr generic argument.Pierre-Marie Pédrot
2016-01-14Removing ident and var generic arguments.Pierre-Marie Pédrot
2016-01-11CLEANUP: removing unused fieldMatej Kosik
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2016-01-02Use streams rather than strings to handle bullet suggestions.Guillaume Melquiond
2016-01-02Remove some unused functions.Guillaume Melquiond
2016-01-02Reduce dependencies of interface files.Guillaume Melquiond
2016-01-02Remove useless rec flags.Guillaume Melquiond
2016-01-02Simplification of grammar_prod_item type.Pierre-Marie Pédrot
2016-01-02Separation of concern in TacAlias API.Pierre-Marie Pédrot
2015-12-31Do not compose List.length with List.filter.Guillaume Melquiond
2015-12-30External tactics and notations now accept any tactic argument.Pierre-Marie Pédrot
2015-12-28Removing the special status of open_constr generic argument.Pierre-Marie Pédrot
2015-12-27Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Pierre-Marie Pédrot
2015-12-24Removing auto from the tactic AST.Pierre-Marie Pédrot
2015-12-22Do not compose "str" and "to_string" whenever possible.Guillaume Melquiond
2015-12-21Removing ad-hoc interpretation rules for tactic notations and their genarg.Pierre-Marie Pédrot
2015-12-21Changing the toplevel type of the int_or_var generic type to int.Pierre-Marie Pédrot
2015-12-21Removing the now useless genarg generic argument.Pierre-Marie Pédrot
2015-12-21Using dynamic values in tactic evaluation.Pierre-Marie Pédrot
2015-12-18CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedMatej Kosik
2015-12-18CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionMatej Kosik
2015-12-18CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...Matej Kosik
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-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-25Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-20Print Assumptions shows engagement.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 02:29:10 +0000