| Commit message (Expand) | Author | Age |
* | Removing spurious tclWITHHOLES. | Pierre-Marie Pédrot | 2014-08-27 |
* | 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-25 |
* | 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-23 |
* | Removing unused parts of the Goal.sensitive monad. | Pierre-Marie Pédrot | 2014-08-21 |
* | 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-18 |
* | Fixing too restrictive detection of resolution of evars in "apply in" | Hugo Herbelin | 2014-08-16 |
* | Restore the error-handling behavior of [change], which was silently failing | Matthieu Sozeau | 2014-08-14 |
* | In Hipattern: some functions not working modulo evar instantiation. | Arnaud Spiwack | 2014-08-07 |
* | 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-05 |
* | Cleaning of the new implementation of the tactic monad. | Arnaud Spiwack | 2014-08-04 |
* | 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-08-01 |
* | Add an option to solve typeclass goals generated by apply which can't be | Matthieu Sozeau | 2014-07-31 |
* | Restore proper order of effects in letin_tac_gen. Fixes CFGV again. | Matthieu Sozeau | 2014-07-03 |
* | Synchronized names from the "as" clause with the skeleton of the | Hugo Herbelin | 2014-06-30 |
* | 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-28 |
* | 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-25 |
* | 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-24 |
* | 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-23 |
* | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | 2014-06-18 |
* | Check resolution of Metas turned into Evars by pose_all_metas_as_evars | Hugo Herbelin | 2014-06-13 |
* | Passing some tactics to the new monad type. | Pierre-Marie Pédrot | 2014-06-12 |
* | fix handling of side effects in abstract (fixes QArithSternBrocot) | Enrico Tassi | 2014-06-11 |
* | Preserve compatibility on examples such as "intros []." on goals such | Hugo Herbelin | 2014-06-06 |
* | Collecting in Namegen those conventional default names that are used in diffe... | Hugo Herbelin | 2014-06-04 |
* | 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-31 |
* | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau | 2014-05-26 |
* | Moving the "specialize" tactic out of the AST. Also removed an obsolete | Pierre-Marie Pédrot | 2014-05-22 |
* | Code cleaning & factorizing functions in Equality. | Pierre-Marie Pédrot | 2014-05-09 |
* | 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 |