| Age | Commit message (Expand) | Author |
|---|
| 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-29 | Clean up obsolete comment. | Arnaud Spiwack |
| 2014-07-28 | CPS-style tactic matching. We use the tactic monad as the target of the CPS. | Pierre-Marie Pédrot |
| 2014-07-25 | A slightly more fine grained way to check whether a TACTIC EXTEND is global o... | Arnaud Spiwack |
| 2014-07-24 | Distinguish tactics t1;t2 and t1;[t2..]. | Arnaud Spiwack |
| 2014-07-13 | Adding a "time" tactical for benchmarking purposes. In case the tactic | Hugo Herbelin |
| 2014-07-10 | Fix a oversight in 5bf9e67b . | Arnaud Spiwack |
| 2014-07-07 | Revert "time tac" (committed by mistake). | Hugo Herbelin |
| 2014-07-07 | time tac | Hugo Herbelin |
| 2014-07-03 | More efficient implementation of Ltac match, by inlining a stream map. | Pierre-Marie Pédrot |
| 2014-07-01 | Fixing the place where to insert a space in "Tactic failure" | Hugo Herbelin |
| 2014-06-30 | Useless keeping of dirpath in tactic aliases. | Pierre-Marie Pédrot |
| 2014-06-23 | Fix semantics of change p with c to typecheck c at each specific occurrence o... | Matthieu Sozeau |
| 2014-06-22 | Less goal-entering. | Pierre-Marie Pédrot |
| 2014-06-19 | Adding a raw_goals primitive for Tacinterp. | Pierre-Marie Pédrot |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-07 | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot |
| 2014-06-06 | 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-03 | The tactic interpreter now uses a new type of tactics, through | Pierre-Marie Pédrot |
| 2014-05-31 | Upgrade Matthieu's new_revert as the "revert" (a "unit tactic"). | Hugo Herbelin |
| 2014-05-24 | 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-22 | Moving the "specialize" tactic out of the AST. Also removed an obsolete | 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 | 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-16 | Moving argument-free tactics out of the AST into a dedicated | Pierre-Marie Pédrot |
| 2014-05-09 | Refresh universes for Ltac's type_of, as the term can be used anywhere, | Matthieu Sozeau |
| 2014-05-08 | 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-06 | - 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-04-27 | Rewriting [lapply] tactic in the new monad. | Pierre-Marie Pédrot |
| 2014-04-25 | 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-24 | Writing tclABSTRACT in the new monad. In particular the unsafe status is now | Pierre-Marie Pédrot |
| 2014-04-20 | Fixing bug #3285. | Pierre-Marie Pédrot |
| 2014-04-14 | Closing bug #3260 | Julien Forest |
| 2014-03-19 | 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-05 | Remove some dead-code (thanks to ocaml warnings) | Pierre Letouzey |
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
