aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.mli
AgeCommit message (Expand)Author
2015-09-08Fixing "pose proof (H ...) as H" and "assert (H:=H ...) which were supposedHugo Herbelin
2015-04-10Fix #3590 for good this time, by changing the API, change's argument nowMatthieu Sozeau
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-01-12Update headers.Maxime Dénès
2014-12-07Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Hugo Herbelin
2014-11-22Simplifying code of functional induction.Hugo Herbelin
2014-11-22Writing intro_replacing in the new monad.Pierre-Marie Pédrot
2014-11-21Writing Tactics.keep in the new monad.Pierre-Marie Pédrot
2014-11-16Fixing side bug in db37c9f3f32ae7 delaying interpretation of theHugo Herbelin
2014-11-09Removing the unused boolean flag from the move tactic implementation.Pierre-Marie Pédrot
2014-11-05Writing the raw introduction tactic in the new monad.Pierre-Marie Pédrot
2014-11-03Writing rename_hyps in the new monad.Pierre-Marie Pédrot
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-22Remove the deprecated open-constr based refine.Arnaud Spiwack
2014-10-13Fixing "change" and "fold" after convert_hyp/convert_concl moved toHugo Herbelin
2014-10-09A version of convert_concl and convert_hyp in new proof engine.Hugo Herbelin
2014-10-07Splitting out of auto.ml a file hints.ml dedicated to hints so as toHugo Herbelin
2014-09-17Fix bug #3633 properly, by delaying the interpetation of constrs inMatthieu Sozeau
2014-09-15Add a "Hint Mode ref (+ | -)*" hint for setting a global modeMatthieu Sozeau
2014-09-11Other bugs with "inversion as" (collision between user-provided names and gen...Hugo Herbelin
2014-09-10Fixing inversion after having fixed intros_replacingHugo Herbelin
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-04Reimplementing the clearbody tactic.Pierre-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-18A few more comments in tactics.mli and hippatern.ml.Hugo 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-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-01Removing some tactic compatibility layer.Pierre-Marie Pédrot
2014-06-23Fix semantics of change p with c to typecheck c at each specific occurrence o...Matthieu Sozeau
2014-06-12Passing some tactics to the new monad type.Pierre-Marie Pédrot
2014-05-31Fixing introduction patterns * and ** when used in a branch so that they do n...Hugo Herbelin
2014-05-31Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").Hugo Herbelin
2014-05-22Moving the "specialize" tactic out of the AST. Also removed an obsoletePierre-Marie Pédrot
2014-05-09Code cleaning & factorizing functions in Equality.Pierre-Marie Pédrot
2014-05-08Encapsulating some clausenv uses. This simplifies the control flow of somePierre-Marie Pédrot
2014-05-08Isolating a function "make_abstraction", new name of "letin_abstract",Hugo Herbelin
2014-05-08Renaming new_induct -> induction; new_destruct -> destruct.Hugo Herbelin
2014-05-08- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-27Rewriting [lapply] tactic in the new monad.Pierre-Marie Pédrot
2014-04-24Writing tclABSTRACT in the new monad. In particular the unsafe status is nowPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:21:25 +0000