| Commit message (Expand) | Author | Age |
|---|
| * | 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 |
| * | 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-29 |
| * | Clean up obsolete comment. | Arnaud Spiwack | 2014-07-29 |
| * | CPS-style tactic matching. We use the tactic monad as the target of the CPS. |  Pierre-Marie Pédrot | 2014-07-28 |
| * | A slightly more fine grained way to check whether a TACTIC EXTEND is global o... | Arnaud Spiwack | 2014-07-25 |
| * | Distinguish tactics t1;t2 and t1;[t2..]. | Arnaud Spiwack | 2014-07-24 |
| * | Adding a "time" tactical for benchmarking purposes. In case the tactic |  Hugo Herbelin | 2014-07-13 |
| * | Fix a oversight in 5bf9e67b . | Arnaud Spiwack | 2014-07-10 |
| * | Revert "time tac" (committed by mistake). | Hugo Herbelin | 2014-07-07 |
| * | time tac | Hugo Herbelin | 2014-07-07 |
| * | More efficient implementation of Ltac match, by inlining a stream map. | Pierre-Marie Pédrot | 2014-07-03 |
| * | Fixing the place where to insert a space in "Tactic failure" | Hugo Herbelin | 2014-07-01 |
| * | Useless keeping of dirpath in tactic aliases. | Pierre-Marie Pédrot | 2014-06-30 |
| * | Fix semantics of change p with c to typecheck c at each specific occurrence o... |  Matthieu Sozeau | 2014-06-23 |
| * | Less goal-entering. | Pierre-Marie Pédrot | 2014-06-22 |
| * | Adding a raw_goals primitive for Tacinterp. | Pierre-Marie Pédrot | 2014-06-19 |
| * | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | 2014-06-18 |
| * | Removing dead code. | Pierre-Marie Pédrot | 2014-06-17 |
| * | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot | 2014-06-07 |
| * | Fixes the lost evars when interpreting a change with pattern tactic. | Arnaud Spiwack | 2014-06-06 |
| * | Moving the [split] tactic out of the AST. | Pierre-Marie Pédrot | 2014-06-06 |
| * | The tactic interpreter now uses a new type of tactics, through | Pierre-Marie Pédrot | 2014-06-03 |
| * | Upgrade Matthieu's new_revert as the "revert" (a "unit tactic"). | Hugo Herbelin | 2014-05-31 |
| * | Revert "Chasing the goal entering backward while interpreting tactics. This r... | Pierre-Marie Pédrot | 2014-05-24 |
| * | Chasing the goal entering backward while interpreting tactics. This required | Pierre-Marie Pédrot | 2014-05-24 |
| * | Moving the "specialize" tactic out of the AST. Also removed an obsolete | 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 |
| * | Tactics declared through TACTIC EXTEND that are of the form | Pierre-Marie Pédrot | 2014-05-20 |
| * | Tentative to add constr-using primitive tactics without grammar rules. | Pierre-Marie Pédrot | 2014-05-20 |
| * | Moving argument-free tactics out of the AST into a dedicated | Pierre-Marie Pédrot | 2014-05-16 |
| * | Refresh universes for Ltac's type_of, as the term can be used anywhere, | Matthieu Sozeau | 2014-05-09 |
| * | Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic." | Hugo Herbelin | 2014-05-08 |
| * | Avoid "revert" to retype-check the goal, and move it to a "new" tactic. | Hugo Herbelin | 2014-05-08 |
| * | Isolating a function "make_abstraction", new name of "letin_abstract", | Hugo Herbelin | 2014-05-08 |
| * | Code cleaning in Tacinterp: factorizing some uses of tclEVARS. | Pierre-Marie Pédrot | 2014-05-08 |
| * | - Fix eq_constr_universes restricted to Sorts.equal | Matthieu Sozeau | 2014-05-06 |
| * | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | 2014-05-06 |
| * | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
| * | Rewriting [lapply] tactic in the new monad. | Pierre-Marie Pédrot | 2014-04-27 |
| * | Removing useless try-with clauses in Goal.enter variants. | Pierre-Marie Pédrot | 2014-04-25 |
| * | Fixing various backtrace recordings. | Pierre-Marie Pédrot | 2014-04-25 |
| * | Writing tclABSTRACT in the new monad. In particular the unsafe status is now | Pierre-Marie Pédrot | 2014-04-24 |
| * | Fixing bug #3285. | Pierre-Marie Pédrot | 2014-04-20 |
| * | Closing bug #3260 |  Julien Forest | 2014-04-14 |
| * | Using non-normalized goals in tactic interpretation. | Pierre-Marie Pédrot | 2014-03-19 |
| * | Adding phantom types to discriminate normalized goals, and adding a way to | Pierre-Marie Pédrot | 2014-03-19 |
Arnaud Spiwack
Pierre-Marie Pédrot
Hugo Herbelin
Matthieu Sozeau
Julien Forest