aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
...
* | | | | Removing constr generic argument.Gravatar Pierre-Marie Pédrot2016-01-14
* | | | | Removing ident and var generic arguments.Gravatar Pierre-Marie Pédrot2016-01-14
* | | | | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | | | | mergeGravatar Matej Kosik2016-01-11
|\ \ \ \ \
| * | | | | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | | | | Use streams rather than strings to handle bullet suggestions.Gravatar Guillaume Melquiond2016-01-02
* | | | | | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
* | | | | | Reduce dependencies of interface files.Gravatar Guillaume Melquiond2016-01-02
* | | | | | Remove useless rec flags.Gravatar Guillaume Melquiond2016-01-02
* | | | | | Simplification of grammar_prod_item type.Gravatar Pierre-Marie Pédrot2016-01-02
* | | | | | Separation of concern in TacAlias API.Gravatar Pierre-Marie Pédrot2016-01-02
* | | | | | Do not compose List.length with List.filter.Gravatar Guillaume Melquiond2015-12-31
* | | | | | External tactics and notations now accept any tactic argument.Gravatar Pierre-Marie Pédrot2015-12-30
* | | | | | Removing the special status of open_constr generic argument.Gravatar Pierre-Marie Pédrot2015-12-28
* | | | | | Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-12-27
* | | | | | Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
* | | | | | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
* | | | | | Removing ad-hoc interpretation rules for tactic notations and their genarg.Gravatar Pierre-Marie Pédrot2015-12-21
* | | | | | Changing the toplevel type of the int_or_var generic type to int.Gravatar Pierre-Marie Pédrot2015-12-21
* | | | | | Removing the now useless genarg generic argument.Gravatar Pierre-Marie Pédrot2015-12-21
* | | | | | Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
|/ / / / /
* | | | | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
* | | | | CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionGravatar Matej Kosik2015-12-18
* | | | | CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...Gravatar Matej Kosik2015-12-18
* | | | | CLEANUP: Vernacexpr.vernac_exprGravatar Matej Kosik2015-12-18
* | | | | Tying the loop in tactic printing API.Gravatar Pierre-Marie Pédrot2015-12-18
* | | | | Getting rid of some hardwired generic arguments.Gravatar Pierre-Marie Pédrot2015-12-17
* | | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-08
|\| | | |
* | | | | Moving extended_rel_vect/extended_rel_list to the kernel.Gravatar Hugo Herbelin2015-12-05
* | | | | Getting rid of the dynamic node of the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-04
* | | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\ \ \ \ \
| | * | | | 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
* | | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\| | | |
| * | | | Adding syntax "Show id" to show goal named id (shelved or not).Gravatar Hugo Herbelin2015-11-02
| | * | | Make the code of compare functions linear in the number of constructors.Gravatar Arnaud Spiwack2015-10-29
* | | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\| | | | | |/ / / |/| | |
| * | | Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
| * | | Printing of @{} instances for polymorphic references in Print and About.Gravatar Matthieu Sozeau2015-10-28
* | | | Type delayed_open_constr is now monotonic.Gravatar Pierre-Marie Pédrot2015-10-19
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|\| | |
| * | | 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
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-06
|\| | |
| * | | Univs: fix printing bug #3797.Gravatar Matthieu Sozeau2015-10-05
| | | * Show assumptions of well-foundedness in `Print Assumptions`Gravatar Arnaud Spiwack2015-09-25
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-09-25
|\| | |
| | | * Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...Gravatar Arnaud Spiwack2015-09-25
| * | | Print Assumptions shows engagement.Gravatar Maxime Dénès2015-09-20