aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.mli
AgeCommit message (Expand)Author
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
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-03-31Removing the Change_evar refiner rule.Pierre-Marie Pédrot
2014-03-31Removing dead code in Tactics.Pierre-Marie Pédrot
2014-03-28Define Tactics.bring_hyps in the new monad.Pierre-Marie Pédrot
2014-03-26Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.Pierre-Marie Pédrot
2014-03-26Removing Tacmach compatibility layer in Inv.Pierre-Marie Pédrot
2014-03-26Moving some tactic code to the new engine.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-12-02Writing [cut] tactic using the new monad.Pierre-Marie Pédrot
2013-11-25Remove the Hiddentac module.Arnaud Spiwack
2013-11-08Porting Tactics.assumption to the new engine.ppedrot
2013-11-02A whole new implemenation of the refine tactic.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-08-08State Transaction Machinegareuselesinge
2013-07-09Revising r16550 about providing intro patterns for applying injection:herbelin
2013-06-02Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as anherbelin
2013-05-12Use the Hook module here and there.ppedrot
2013-04-29Merging Context and Sign.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 00:47:25 +0000