| Age | Commit message (Expand) | Author |
|---|
| 2014-08-07 | In Hipattern: some functions not working modulo evar instantiation. | Arnaud Spiwack |
| 2014-08-05 | Experimentally adding an option for automatically erasing an | Hugo Herbelin |
| 2014-08-05 | Adding a syntax "enough" for the variant of "assert" with the order of | Hugo Herbelin |
| 2014-08-05 | A new step in the new "standard" naming policy for propositional hypotheses | Hugo Herbelin |
| 2014-08-04 | Cleaning of the new implementation of the tactic monad. | Arnaud Spiwack |
| 2014-08-01 | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin |
| 2014-08-01 | Removing more tactic compatibility layer. | Pierre-Marie Pédrot |
| 2014-08-01 | Removing some tactic compatibility layer. | Pierre-Marie Pédrot |
| 2014-07-31 | Add an option to solve typeclass goals generated by apply which can't be | Matthieu Sozeau |
| 2014-07-03 | Restore proper order of effects in letin_tac_gen. Fixes CFGV again. | Matthieu Sozeau |
| 2014-06-30 | Synchronized names from the "as" clause with the skeleton of the | Hugo Herbelin |
| 2014-06-28 | Small refinement about whether it is tolerated for compatibility that | Hugo Herbelin |
| 2014-06-28 | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin |
| 2014-06-28 | Extra check for indirect dependency when abstracting a term which is | Hugo Herbelin |
| 2014-06-28 | Made the subterm finding function make_abstraction independent of the | Hugo Herbelin |
| 2014-06-25 | Incorrect folding of evars in let_tac_gen made remember fail to store | Matthieu Sozeau |
| 2014-06-25 | In exact check, use e_type_of to ensure that universe constraints necessary | Matthieu Sozeau |
| 2014-06-24 | Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it | Pierre-Marie Pédrot |
| 2014-06-24 | Clenvtac.res_pf is in the new tactic monad. | Pierre-Marie Pédrot |
| 2014-06-23 | Removing opens to Clenvtac to track its use more easily. | 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-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau |
| 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 handling of side effects in abstract (fixes QArithSternBrocot) | Enrico Tassi |
| 2014-06-06 | Preserve compatibility on examples such as "intros []." on goals such | Hugo Herbelin |
| 2014-06-04 | Collecting in Namegen those conventional default names that are used in diffe... | 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-26 | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau |
| 2014-05-22 | Moving the "specialize" tactic out of the AST. Also removed an obsolete | Pierre-Marie Pédrot |
| 2014-05-09 | Code cleaning & factorizing functions in Equality. | Pierre-Marie Pédrot |
| 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 | 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-06 | Use new tactic combinators in tclABSTRACT, to avoid blowup when using V82.tac... | 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 eq_constr_universes restricted to Sorts.equal | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 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 | Better hashconsing of levels and universes, working with modules. | 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 |
