| Commit message (Expand) | Author | Age |
... | |
* | Moving the TacExtend node from atomic to plain tactics. | Pierre-Marie Pédrot | 2014-08-18 |
* | Fixing parsing of bullets after a "...". | Hugo Herbelin | 2014-08-12 |
* | 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-07 |
* | Removing "intros untils" from the AST. | Pierre-Marie Pédrot | 2014-08-06 |
* | 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-05 |
* | 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-08-01 |
* | 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-29 |
* | Qualified ML tactic names. The plugin name is used to discriminate | Pierre-Marie Pédrot | 2014-07-27 |
* | Distinguish tactics t1;t2 and t1;[t2..]. | Arnaud Spiwack | 2014-07-24 |
* | Adding a new "Locate Term" command, distinct from the raw "Locate" command. | Pierre-Marie Pédrot | 2014-07-21 |
* | Adding a "time" tactical for benchmarking purposes. In case the tactic | Hugo Herbelin | 2014-07-13 |
* | Revert "time tac" (committed by mistake). | Hugo Herbelin | 2014-07-07 |
* | time tac | Hugo Herbelin | 2014-07-07 |
* | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau | 2014-07-01 |
* | Fixing #3390 (mismatch simple_tactic/tactic0 leading to segfault). | Hugo Herbelin | 2014-06-21 |
* | - Add "Show Universes" to print information about universes during a proof. | Matthieu Sozeau | 2014-06-16 |
* | Fix bug #3289 | Matthieu Sozeau | 2014-06-11 |
* | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau | 2014-06-10 |
* | Remove the syntax [Vernac1. Vernac2. … Vernacn. ]. | Arnaud Spiwack | 2014-06-06 |
* | Moving the [split] tactic out of the AST. | Pierre-Marie Pédrot | 2014-06-06 |
* | - Better parsing and printing of named universes: Type{ident} and foo@{(ident... | Matthieu Sozeau | 2014-06-04 |
* | - Allow parsing of @const@{instance} for specifying universe instances of pol... | Matthieu Sozeau | 2014-06-04 |
* | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau | 2014-06-04 |
* | Removing symmetry from the atomic tactics. | Pierre-Marie Pédrot | 2014-06-02 |
* | Fixing commit 9cef834. The parsing rules were generating an empty list, | Pierre-Marie Pédrot | 2014-05-26 |
* | Complying with reference manual for the syntax of exists/eexists, i.e. | Hugo Herbelin | 2014-05-24 |
* | Moving the "specialize" tactic out of the AST. Also removed an obsolete | Pierre-Marie Pédrot | 2014-05-22 |
* | Removing useless use of metaids in tactic AST. | Pierre-Marie Pédrot | 2014-05-22 |
* | Removing decompose record / sum from the tactic AST. | Pierre-Marie Pédrot | 2014-05-21 |
* | Moving left & right tactics out of the AST. | Pierre-Marie Pédrot | 2014-05-21 |
* | Moving (e)transitivity out of the AST. | Pierre-Marie Pédrot | 2014-05-20 |
* | Tentative to add constr-using primitive tactics without grammar rules. | Pierre-Marie Pédrot | 2014-05-20 |
* | Adding way to get the list of the accepted tactic notation arguments. | Pierre-Marie Pédrot | 2014-05-17 |
* | Moving argument-free tactics out of the AST into a dedicated | Pierre-Marie Pédrot | 2014-05-16 |
* | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot | 2014-05-12 |
* | Moving the ML tactic extension mechanism to a Libobject-based one. | Pierre-Marie Pédrot | 2014-05-12 |
* | Cleanup before merge with the trunk | Matthieu Sozeau | 2014-05-06 |