| Age | Commit message (Expand) | Author |
|---|
| 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-17 | Improve hotspot in Auto. | Pierre-Marie Pédrot |
| 2014-06-13 | Check resolution of Metas turned into Evars by pose_all_metas_as_evars | Hugo Herbelin |
| 2014-06-12 | Passing some tactics to the new monad type. | Pierre-Marie Pédrot |
| 2014-06-11 | Fix bug #3291, stack overflow in rewrite. | Matthieu Sozeau |
| 2014-06-11 | Fix bug #3289 | Matthieu Sozeau |
| 2014-06-11 | In generalized rewrite, avoid retyping completely and constantly the conclusi... | Matthieu Sozeau |
| 2014-06-11 | fix handling of side effects in abstract (fixes QArithSternBrocot) | Enrico Tassi |
| 2014-06-08 | Moving hook code from Future to Lemmas. This seemed to disrupt compilation of | Pierre-Marie Pédrot |
| 2014-06-08 | Enforce a correct exception handling in declaration_hooks | Enrico Tassi |
| 2014-06-07 | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot |
| 2014-06-06 | Preserve compatibility on examples such as "intros []." on goals such | Hugo Herbelin |
| 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-04 | Collecting in Namegen those conventional default names that are used in diffe... | Hugo Herbelin |
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau |
| 2014-06-03 | The tactic interpreter now uses a new type of tactics, through | Pierre-Marie Pédrot |
| 2014-06-02 | Removing symmetry from the atomic tactics. | Pierre-Marie Pédrot |
| 2014-05-31 | More on injection over a projectable "existT". - Fixing syntax "injection ...... | Hugo Herbelin |
| 2014-05-31 | Fixing introduction patterns * and ** when used in a branch so that they do n... | Hugo Herbelin |
| 2014-05-31 | Upgrade Matthieu's new_revert as the "revert" (a "unit tactic"). | Hugo Herbelin |
| 2014-05-27 | Removing a tclSENSITIVE from rewrite. | Pierre-Marie Pédrot |
| 2014-05-26 | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau |
| 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-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 | Allowing Ltac definitions that may be unusable because of a built-in | 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-18 | When discrimination is not possible, try to project. | Maxime Dénès |
| 2014-05-18 | Suggest Set Injection On Proofs in error message for injection. | Maxime Dénès |
| 2014-05-18 | Restored old behavior of injection on proofs by default. | Maxime Dénès |
| 2014-05-16 | Moving argument-free tactics out of the AST into a dedicated | Pierre-Marie Pédrot |
| 2014-05-15 | poly: remove unused attribute to STM nodes and vernac classificaiton | Enrico Tassi |
| 2014-05-12 | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot |
| 2014-05-09 | Code cleaning & factorizing functions in Equality. | Pierre-Marie Pédrot |
| 2014-05-09 | Update and start testing rewrite-in-type code. | Matthieu Sozeau |
| 2014-05-09 | Refresh universes for Ltac's type_of, as the term can be used anywhere, | Matthieu Sozeau |
| 2014-05-08 | Encapsulating some clausenv uses. This simplifies the control flow of some | Pierre-Marie Pédrot |
| 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 | Simplification and improvement of "subst x" in such a way that it | Hugo Herbelin |
| 2014-05-08 | Renaming new_induct -> induction; new_destruct -> destruct. | Hugo Herbelin |
| 2014-05-08 | Little reorganization of generalize tactics code w/o semantic changes. | Hugo Herbelin |
