| Age | Commit message (Expand) | Author |
|---|
| 2014-12-23 | A global [gfail] tactic which works like [fail] except that it fails even if ... | Arnaud Spiwack |
| 2014-12-23 | Fix compilation error in some configurations. | Arnaud Spiwack |
| 2014-12-19 | Add a backtracking version of Ltac's [match]. | Arnaud Spiwack |
| 2014-12-18 | Proof using: New vernacular to name sets of section variables | Enrico Tassi |
| 2014-12-15 | About now accepts hypothesis names and goal selector. | Pierre Courtieu |
| 2014-12-12 | Add Ltac syntax for the [tclIFCATCH] primitive. | Arnaud Spiwack |
| 2014-12-12 | Extend the syntax of simpl with a delta flag. | Arnaud Spiwack |
| 2014-12-12 | Searchxxx now search also the hypothesis and support goal selector. | Pierre Courtieu |
| 2014-12-11 | Tentatively more informative report of failure when inferring | Hugo Herbelin |
| 2014-12-07 | Improved tracking of the origin of evars. | Hugo Herbelin |
| 2014-11-16 | Enforcing a stronger difference between the two syntaxes "simpl | Hugo Herbelin |
| 2014-11-09 | Removing a unused boolean in the TacMove node of tacexpr AST. | Pierre-Marie Pédrot |
| 2014-11-01 | Add a interpreted level [tacexpr] to [Tacexpr] together with its printer. | Arnaud Spiwack |
| 2014-11-01 | Add [Info] command. | Arnaud Spiwack |
| 2014-10-31 | Feedback message: hold extra info to help routing | Enrico Tassi |
| 2014-10-25 | This commit introduces changes in induction and destruct. | Hugo Herbelin |
| 2014-10-20 | A patch for printing "match" when constructors are defined with let-in | Hugo Herbelin |
| 2014-10-13 | Emit a warning for void Arguments statement (Close 3713) | Enrico Tassi |
| 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-17 | Revert specific syntax for primitive projections, avoiding ugly | Matthieu Sozeau |
| 2014-09-15 | Add a "Hint Mode ref (+ | -)*" hint for setting a global mode | Matthieu Sozeau |
| 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-12 | Replace the list of argument in tacexpr with a single row argument. | Arnaud Spiwack |
| 2014-09-10 | VernacExtend does not dispatch on type anymore. | Pierre-Marie Pédrot |
| 2014-09-09 | Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407) | Enrico Tassi |
| 2014-09-08 | Removing the XML plugin. | Pierre-Marie Pédrot |
| 2014-09-08 | Parsing of Type@{max(i,j)}. | Matthieu Sozeau |
| 2014-09-05 | Ltac's [uconstr] values now use the identifier context to give names to binders. | 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 | Removing the 'inductive' parameter from tacexpr AST. | Pierre-Marie Pédrot |
| 2014-09-01 | Moving the decompose tactic out of the AST. | Pierre-Marie Pédrot |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 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 | 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-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 | [uconstr]: use a closure instead of eager substitution. | Arnaud Spiwack |
| 2014-08-06 | Removing "intros untils" from the AST. | Pierre-Marie Pédrot |
| 2014-08-05 | Uncountably many bullets (+,-,*,++,--,**,+++,...). | Hugo Herbelin |
