aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacticals.mli
AgeCommit message (Expand)Author
2016-06-14Goal selectors are now tacticals and can be used as such.Cyprien Mangin
2016-02-16Tacticals: typo in a commentPierre Letouzey
2016-01-21New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).Hugo Herbelin
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-21Stronger invariants on the use of the introduction pattern (pat1,...,patn).Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-27Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Pierre-Marie Pédrot
2015-10-20Indexing Proofview.goals with a stage.Pierre-Marie Pédrot
2015-02-10More expressive API for tclWITHHOLES.Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-12Add Ltac syntax for the [tclIFCATCH] primitive.Arnaud Spiwack
2014-12-08Constructor tactics backtracking is done using [Tacticals.New] rather than [P...Arnaud Spiwack
2014-11-20Adding locations to tclZEROMSG.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-18Reorganisation of intropattern codeHugo Herbelin
2014-07-13Adding a "time" tactical for benchmarking purposes. In case the tacticHugo Herbelin
2014-07-07Revert "time tac" (committed by mistake).Hugo Herbelin
2014-07-07time tacHugo Herbelin
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-04-22Using the new monad tactic in Inv.Pierre-Marie Pédrot
2014-04-22Removing tactic compatibility layer from Elim.Pierre-Marie Pédrot
2014-04-22Simplifying interface of elimination tactics. They used dummy clausenvs, andPierre-Marie Pédrot
2014-03-31Removing the Change_evar refiner rule.Pierre-Marie Pédrot
2014-03-27Removing tactic compatibility layer from Eqdecide.Pierre-Marie Pédrot
2014-03-26Removing tactic compatibility layer in Equality.Pierre-Marie Pédrot
2014-03-26Removing Tacmach compatibility layer in Inv.Pierre-Marie Pédrot
2014-03-26Removing tactic compatibility layer from Inv.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-11-14Implementation of Ltac's match and match goal fully based on IStream.aspiwack
2013-11-04Fix ltac's progress tactical: requires progress in each goal.aspiwack
2013-11-02Update comments.aspiwack
2013-11-02Adds an experimental exactly_once tactical.aspiwack
2013-11-02Adds a tactical once.aspiwack
2013-11-02Added the tactical "tac1 + tac2".aspiwack
2013-11-02Bases tactics on an IO monad.aspiwack
2013-11-02Uses Proofview.tclEXTEND more sparingly.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2012-12-14Modulification of identifierppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-10-01Added a new tactical infoH tac, that displays the names of hypothesis created...courtieu
2012-08-08Updating headers.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 02:54:59 +0000