| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-05-08 | - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ... | Matthieu Sozeau |
| 2014-05-08 | Moving Dnet-related code to tactics/. | Pierre-Marie Pédrot |
| 2014-05-08 | Code cleaning in Tacinterp: factorizing some uses of tclEVARS. | Pierre-Marie Pédrot |
| 2014-05-06 | Cleanup before merge with the trunk | Matthieu Sozeau |
| 2014-05-06 | Use new tactic combinators in tclABSTRACT, to avoid blowup when using V82.tac... | Matthieu Sozeau |
| 2014-05-06 | - Fix treatment of global universe constraints which should be passed along | Matthieu Sozeau |
| 2014-05-06 | Avoid u+k <= v constraints, don't take the sup of an algebraic universe during | Matthieu Sozeau |
| 2014-05-06 | - Fix arity handling in retyping (de Bruijn bug!) | Matthieu Sozeau |
| 2014-05-06 | - Fix eq_constr_universes restricted to Sorts.equal | Matthieu Sozeau |
| 2014-05-06 | Fixes after rebase. The use of pf_constr_of_global is problematic in presence... | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | Adapt Y. Bertot's path on private inductives (now the keyword is "Private"). | Yves Bertot |
| 2014-05-06 | - Fix abstract forgetting about new constraints. | Matthieu Sozeau |
| 2014-05-06 | - Fix handling of polymorphic inductive elimination schemes. | Matthieu Sozeau |
| 2014-05-06 | Various fixes of universe polymorphism and projections when they're set. | Matthieu Sozeau |
| 2014-05-06 | Better hashconsing of levels and universes, working with modules. | Matthieu Sozeau |
| 2014-05-06 | Correct rebase on STM code. Thanks to E. Tassi for help on dealing with | Matthieu Sozeau |
| 2014-05-06 | Rework handling of universes on top of the STM, allowing for delayed | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-30 | Trying to improve the error messages of injection. | Maxime Dénès |
| 2014-04-29 | Injection: do not fail when arguments have sort Prop. | Maxime Dénès |
| 2014-04-27 | Rewriting [lapply] tactic in the new monad. | Pierre-Marie Pédrot |
| 2014-04-27 | Giving true proof-terms in inversion instead of metas. | Pierre-Marie Pédrot |
