aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacticals.mli
AgeCommit message (Expand)Author
2017-04-01Using delayed universe instances in EConstr.Pierre-Marie Pédrot
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Removing most nf_enter in tactics.Pierre-Marie Pédrot
2017-02-14Do not ask for a normalized goal to get hypotheses and conclusions.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers from TacticalsPierre-Marie Pédrot
2017-02-14Cleaning up interfaces.Pierre-Marie Pédrot
2017-02-14Elim API using EConstr.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacticals API using EConstr.Pierre-Marie Pédrot
2017-02-10Proofview: tclINDEPENDENTLEnrico Tassi
2016-09-15Untangling Tacexpr from lower strata.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 16:23:50 +0000