| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-03-02 | Matching --> ConstrMatching (was clashing with OCaml's compiler-libs) | Pierre Letouzey |
| 2014-03-02 | Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code | Pierre Letouzey |
| 2014-03-01 | Removing a fishy use of pervasive equality in Ltac backtrace printing. | Pierre-Marie Pédrot |
| 2014-02-27 | Tacinterp: more refactoring. | Arnaud Spiwack |
| 2014-02-27 | Tacinterp: refactoring using Monad. | Arnaud Spiwack |
| 2014-02-27 | Remove unsafe code (Obj.magic) in Tacinterp. | Arnaud Spiwack |
| 2014-02-27 | Proofview.Notations: Now that (>>=) is free, use it for tclBIND. | Arnaud Spiwack |
| 2014-02-27 | Tacinterp: yet another superfluous enterl. | Arnaud Spiwack |
| 2014-02-27 | Tacinterp: spurious enterl. | Arnaud Spiwack |
| 2014-02-27 | Dead code: eval_ltac_constr. | Arnaud Spiwack |
| 2014-02-25 | Tacinterp: remove the is_value check in Ltac's let-in. | Arnaud Spiwack |
| 2014-02-25 | Tacinterp: fewer enterl still. | Arnaud Spiwack |
