| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-07-11 | Feedback: LoadedFile + Goals | Enrico Tassi |
| 2014-07-09 | Locate: also display some information about module aliasing | Pierre Letouzey |
| 2014-07-07 | Revert "time tac" (committed by mistake). | Hugo Herbelin |
| 2014-07-07 | time tac | Hugo Herbelin |
| 2014-07-01 | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-16 | - Add "Show Universes" to print information about universes during a proof. | Matthieu Sozeau |
| 2014-06-11 | Fix bug #3289 | Matthieu Sozeau |
| 2014-06-10 | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau |
| 2014-06-06 | 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-04 | - 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-05-22 | 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-21 | 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-20 | 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-16 | Moving argument-free tactics out of the AST into a dedicated | Pierre-Marie Pédrot |
| 2014-05-16 | Slightly better printer for native ML tactics, in order to disambiguate | Pierre-Marie Pédrot |
| 2014-05-06 | Print universes in module printing | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | Adapt universe polymorphic branch to new handling of futures for delayed proofs. | Matthieu Sozeau |
