aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacticals.mli
AgeCommit message (Expand)Author
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
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-30info_trivial, info_auto, info_eauto, and debug (trivial|auto)letouzey
2012-03-02Noise for nothingpboutill
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 15:45:43 +0000