| Age | Commit message (Expand) | Author |
|---|
| 2014-10-25 | This commit introduces changes in induction and destruct. | Hugo Herbelin |
| 2014-10-13 | Emit a warning for void Arguments statement (Close 3713) | Enrico Tassi |
| 2014-10-13 | Parsing of "?[" as two tokens (makes ssr compile). | Enrico Tassi |
| 2014-10-07 | Fixing #3687 (inconsistent lexer state after a bullet). | Hugo Herbelin |
| 2014-09-30 | Seeing IntroWildcard as an action intro pattern rather than as a naming pattern | Hugo Herbelin |
| 2014-09-30 | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin |
| 2014-09-29 | Notation: option to attach extra pretty printing rules to notations | Enrico Tassi |
| 2014-09-24 | Using an or_var rather than the hack with loc for coding a pure ident | Hugo Herbelin |
| 2014-09-15 | Add a "Hint Mode ref (+ | -)*" hint for setting a global mode | Matthieu Sozeau |
| 2014-09-13 | Checking typability of evar instances. Using ";" to separate bindings | Hugo Herbelin |
| 2014-09-12 | Add syntax [id]: to apply tactic to goal named id. | Hugo Herbelin |
| 2014-09-12 | Parsing evar instances. | Hugo Herbelin |
| 2014-09-12 | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin |
| 2014-09-10 | VernacExtend does not dispatch on type anymore. | Pierre-Marie Pédrot |
| 2014-09-08 | Removing dead code relative to the XML plugin. | Pierre-Marie Pédrot |
| 2014-09-08 | Removing the XML plugin. | Pierre-Marie Pédrot |
| 2014-09-08 | Parsing of Type@{max(i,j)}. | Matthieu Sozeau |
| 2014-09-04 | Factorize the parsing rules of [Record] and the other kind of type definitions. | Arnaud Spiwack |
| 2014-09-04 | Remove [Infer] option of records. | Arnaud Spiwack |
| 2014-09-04 | Add a [Variant] declaration which allows to write non-recursive variant types. | Arnaud Spiwack |
| 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-08-27 | Fixing bug #3493. | Pierre-Marie Pédrot |
| 2014-08-24 | Removing a unused legacy parsing rule. | Pierre-Marie Pédrot |
| 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 | 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 | Fixing parsing of bullets after a "...". | 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 | 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-05 | Small refactoring: use [uconstr] instead of [constr] when relevant in grammar... | Arnaud Spiwack |
| 2014-08-05 | Properly declare uconstr as an argument for TACTIC EXTEND. | Arnaud Spiwack |
| 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 | Continuing (incomplete) cleaning of Inductiveops. | Hugo Herbelin |
| 2014-08-01 | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin |
| 2014-07-29 | Small refactoring in Ltac parsing rules. | Arnaud Spiwack |
| 2014-07-29 | Allow [uconstr:c] as argument of a tactic. | 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 | Untyped term in tactics: add an grammar entry to construct them. | Arnaud Spiwack |
| 2014-07-27 | Qualified ML tactic names. The plugin name is used to discriminate | Pierre-Marie Pédrot |
| 2014-07-24 | Distinguish tactics t1;t2 and t1;[t2..]. | Arnaud Spiwack |
| 2014-07-21 | Adding a new "Locate Term" command, distinct from the raw "Locate" command. | Pierre-Marie Pédrot |
