| Commit message (Expand) | Author | Age |
|---|
| * | 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 |
| * | 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-05 |
| * | 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-02 |
| * | Removing a fishy use of pervasive equality in Ltac backtrace printing. | Pierre-Marie Pédrot | 2014-03-01 |
| * | 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 |
Arnaud Spiwack
Hugo Herbelin
Pierre-Marie Pédrot
Matthieu Sozeau
Julien Forest
Pierre Letouzey