| Age | Commit message (Expand) | Author |
|---|
| 2014-08-29 | Not using a "cut" in descend_in_conjunctions induced more success. We | Hugo Herbelin |
| 2014-08-27 | Removing spurious tclWITHHOLES. | Pierre-Marie Pédrot |
| 2014-08-25 | Fixing previous commit. | Pierre-Marie Pédrot |
| 2014-08-25 | Fixing a bug introduced in the extension of 'apply in' + simplifying code. | Hugo Herbelin |
| 2014-08-23 | Tactics.is_quantified_hypothesis does not reduce anymore to decide whether | Pierre-Marie Pédrot |
| 2014-08-23 | Tactics.unify in the new monad. | Pierre-Marie Pédrot |
| 2014-08-21 | Removing unused parts of the Goal.sensitive monad. | Pierre-Marie Pédrot |
| 2014-08-18 | Lazy interpretation of patterns so that expressions such as "intros H H'/H" | Hugo Herbelin |
| 2014-08-18 | Adding a new intro-pattern for "apply in" on the fly. Using syntax | Hugo Herbelin |
| 2014-08-18 | Slight simplification of naming of tactics in equality.ml (hopefully). | Hugo Herbelin |
| 2014-08-18 | A reorganization of the "assert" tactics (hopefully uniform naming | Hugo Herbelin |
| 2014-08-18 | Reorganisation of intropattern code | Hugo Herbelin |
| 2014-08-18 | Reorganization of tactics: | Hugo Herbelin |
| 2014-08-16 | Fixing too restrictive detection of resolution of evars in "apply in" | Hugo Herbelin |
| 2014-08-14 | Restore the error-handling behavior of [change], which was silently failing | Matthieu Sozeau |
| 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 |
