aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.ml
AgeCommit message (Expand)Author
2014-09-15Add a "Hint Mode ref (+ | -)*" hint for setting a global modeMatthieu Sozeau
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-09-12Commit 682aa67cc80 about enforcing that apply does not create newHugo Herbelin
2014-09-11Keeping a sub-optimal behavior of intros_possibly_replacing for compatibility...Hugo Herbelin
2014-09-11Other bugs with "inversion as" (collision between user-provided names and gen...Hugo Herbelin
2014-09-10A step towards better differentiating when w_unify is used for subtermHugo Herbelin
2014-09-10More small bugs in intros_replacing.Hugo Herbelin
2014-09-10Fixing inversion after having fixed intros_replacingHugo Herbelin
2014-09-08Fix [induction] wrt inductive records and non-recursive variants.Arnaud Spiwack
2014-09-07Fixing a bug in intros_replacing which was causing inversion notHugo Herbelin
2014-09-06Fixing clearbody : typecheck definitions in context.Pierre-Marie Pédrot
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-09-05Removing the old implementation of clear_body.Pierre-Marie Pédrot
2014-09-05At last a working clearbody!Pierre-Marie Pédrot
2014-09-04Revert the two previous commits. I was testing in the wrong branch.Pierre-Marie Pédrot
2014-09-04Removing the old implementation of clear_body.Pierre-Marie Pédrot
2014-09-04Reimplementing the clearbody tactic.Pierre-Marie Pédrot
2014-09-04Proofview refiner is now type-safe by default.Pierre-Marie Pédrot
2014-09-04Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.Pierre-Marie Pédrot
2014-09-03Yes another remaining clearing bug with 'apply in'.Hugo Herbelin
2014-09-02Another fix than 19a7a5789c to avoid descend_in_conjunction to useHugo Herbelin
2014-08-29Not using a "cut" in descend_in_conjunctions induced more success. WeHugo Herbelin
2014-08-27Removing spurious tclWITHHOLES.Pierre-Marie Pédrot
2014-08-25Fixing previous commit.Pierre-Marie Pédrot
2014-08-25Fixing a bug introduced in the extension of 'apply in' + simplifying code.Hugo Herbelin
2014-08-23Tactics.is_quantified_hypothesis does not reduce anymore to decide whetherPierre-Marie Pédrot
2014-08-23Tactics.unify in the new monad.Pierre-Marie Pédrot
2014-08-21Removing unused parts of the Goal.sensitive monad.Pierre-Marie Pédrot
2014-08-18Lazy interpretation of patterns so that expressions such as "intros H H'/H"Hugo Herbelin
2014-08-18Adding a new intro-pattern for "apply in" on the fly. Using syntaxHugo Herbelin
2014-08-18Slight simplification of naming of tactics in equality.ml (hopefully).Hugo Herbelin
2014-08-18A reorganization of the "assert" tactics (hopefully uniform namingHugo Herbelin
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-08-18Reorganization of tactics:Hugo Herbelin
2014-08-16Fixing too restrictive detection of resolution of evars in "apply in"Hugo Herbelin
2014-08-14Restore the error-handling behavior of [change], which was silently failingMatthieu Sozeau
2014-08-07In Hipattern: some functions not working modulo evar instantiation.Arnaud Spiwack
2014-08-05Experimentally adding an option for automatically erasing anHugo Herbelin
2014-08-05Adding a syntax "enough" for the variant of "assert" with the order ofHugo Herbelin
2014-08-05A new step in the new "standard" naming policy for propositional hypothesesHugo Herbelin
2014-08-04Cleaning of the new implementation of the tactic monad.Arnaud Spiwack
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-08-01Removing more tactic compatibility layer.Pierre-Marie Pédrot
2014-08-01Removing some tactic compatibility layer.Pierre-Marie Pédrot
2014-07-31Add an option to solve typeclass goals generated by apply which can't beMatthieu Sozeau
2014-07-03Restore proper order of effects in letin_tac_gen. Fixes CFGV again.Matthieu Sozeau
2014-06-30Synchronized names from the "as" clause with the skeleton of theHugo Herbelin
2014-06-28Small refinement about whether it is tolerated for compatibility thatHugo Herbelin
2014-06-28Moved code for finding subterms (pattern, induction, set, generalize, ...)Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 12:05:30 +0000