| Age | Commit message (Expand) | Author |
|---|
| 2014-09-04 | Remove [Infer] option of records. | Arnaud Spiwack |
| 2014-09-04 | Inductive and CoInductive records are printed correctly. | Arnaud Spiwack |
| 2014-09-04 | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack |
| 2014-09-04 | Add a [Variant] declaration which allows to write non-recursive variant types. | Arnaud Spiwack |
| 2014-09-03 | Fixing printing of unreachable local tactics. | Pierre-Marie Pédrot |
| 2014-09-02 | Cleaning code in Pptactic. | Pierre-Marie Pédrot |
| 2014-09-02 | Removing [revert] tactic from the AST. | Pierre-Marie Pédrot |
| 2014-09-01 | Moving the decompose tactic out of the AST. | Pierre-Marie Pédrot |
| 2014-09-01 | Coqide prints succesive hyps of the same type on 1 line | Pierre Boutillier |
| 2014-08-30 | Simplify even further the declaration of primitive projections, | Matthieu Sozeau |
| 2014-08-29 | Type-safe version of genarg list / pair / opt functions. | Pierre-Marie Pédrot |
| 2014-08-29 | Simplification of Genarg unpackers. | Pierre-Marie Pédrot |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-08-21 | Improve consistency of whitespace (beautifier). | Xavier Clerc |
| 2014-08-21 | Improve consistency of whitespace (beautifier). | Xavier Clerc |
| 2014-08-21 | Space after [identity] coercion keywords (beautifier). | Xavier Clerc |
| 2014-08-21 | Avoid redundant spaces (beautifier). | Xavier Clerc |
| 2014-08-21 | Do not drop the locality qualifier (beautifier). | Xavier Clerc |
| 2014-08-18 | Lazy interpretation of patterns so that expressions such as "intros H H'/H" | Hugo Herbelin |
| 2014-08-18 | Adding a new intro-pattern for "apply in" on the fly. Using syntax | Hugo Herbelin |
| 2014-08-18 | Reorganisation of intropattern code | Hugo Herbelin |
| 2014-08-18 | Refine patch for behavior of unify_to_subterm to allow backtracking on | Matthieu Sozeau |
| 2014-08-18 | Moving the TacAlias node out of atomic tactics. | Pierre-Marie Pédrot |
| 2014-08-18 | Moving the TacExtend node from atomic to plain tactics. | Pierre-Marie Pédrot |
| 2014-08-12 | A couple of fixes/improvements in -beautify, but backtracking on | Hugo Herbelin |
| 2014-08-07 | Removing simple induction / destruct from the AST. | Pierre-Marie Pédrot |
| 2014-08-07 | Instead of relying on a trick to make the constructor tactic parse, put | Pierre-Marie Pédrot |
| 2014-08-07 | Removing the "constructor" tactic from the AST. | Pierre-Marie Pédrot |
| 2014-08-06 | Removing "intros untils" from the AST. | Pierre-Marie Pédrot |
| 2014-08-05 | Uncountably many bullets (+,-,*,++,--,**,+++,...). | Hugo Herbelin |
| 2014-08-05 | Preliminary re-installation of notation interpretation in beautifying mode. | Hugo Herbelin |
| 2014-08-05 | Fixing a few beautifying bugs. | Hugo Herbelin |
| 2014-08-05 | Experimentally adding an option for automatically erasing an | Hugo Herbelin |
| 2014-08-05 | Adding a syntax "enough" for the variant of "assert" with the order of | Hugo Herbelin |
| 2014-08-05 | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi |
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-08-01 | New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal. | Arnaud Spiwack |
| 2014-08-01 | Add [numgoal] to Ltac. | Arnaud Spiwack |
| 2014-08-01 | Fix typo in cf04daec997. | Arnaud Spiwack |
| 2014-07-29 | Untyped terms in tactic: function [type_term c] to give a typed version of [c]. | Arnaud Spiwack |
| 2014-07-29 | Add a type of untyped term to Ltac's value. | Arnaud Spiwack |
| 2014-07-27 | Qualified ML tactic names. The plugin name is used to discriminate | Pierre-Marie Pédrot |
| 2014-07-25 | Removing dead code relative to or_metaid. | Pierre-Marie Pédrot |
| 2014-07-24 | Distinguish tactics t1;t2 and t1;[t2..]. | Arnaud Spiwack |
| 2014-07-24 | Fix misleading pretty-printing of information for non-universe-polymorphic | Matthieu Sozeau |
| 2014-07-21 | Missing space in pretty-printer | Pierre-Marie Pédrot |
| 2014-07-21 | Unifying locate code, also making it more powerful: it is now able to find | Pierre-Marie Pédrot |
| 2014-07-21 | Adding a new "Locate Term" command, distinct from the raw "Locate" command. | Pierre-Marie Pédrot |
| 2014-07-21 | More complete printing of Ltac location, akin to the term-dedicated Locate co... | Pierre-Marie Pédrot |
| 2014-07-13 | Adding a "time" tactical for benchmarking purposes. In case the tactic | Hugo Herbelin |
