aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacticals.ml
AgeCommit message (Expand)Author
2016-10-14Fix bug #5139: Anomalies should not be caught by || / try.Pierre-Marie Pédrot
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-24Optimize the subst tactic.Pierre-Marie Pédrot
2016-06-14Goal selectors are now tacticals and can be used as such.Cyprien Mangin
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
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-21Fixing some problems with double induction.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-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-17More optimizations of [Clenv.clenv_fchain].Pierre-Marie Pédrot
2015-10-29Removing some goal unsafeness in inductive schemes.Pierre-Marie Pédrot
2015-10-20Proofview.Goal.sigma returns an indexed evarmap.Pierre-Marie Pédrot
2015-10-20Indexing Proofview.goals with a stage.Pierre-Marie Pédrot
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-10-02Univs: fix many evar_map initializations and leaks.Matthieu Sozeau
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-23Using tclZEROMSG instead of tclZERO in several places.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
2015-01-03Fixing #3896 (incorrect sigma given to printer).Hugo Herbelin
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-12Add Ltac syntax for the [tclIFCATCH] primitive.Arnaud Spiwack
2014-12-11Tentatively more informative report of failure when inferringHugo Herbelin
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-11-02Plural and singular forms in error messages.Hugo Herbelin
2014-10-22Proofview: split [V82] module into [Unsafe] and [V82].Arnaud Spiwack
2014-09-08Display number of available goals in "incorrect number of goals" error message.Arnaud Spiwack
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-08-28Simplification of the tclCHECKINTERRUPT tactic.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-18Improving error message when applying rewrite to an expression which is not a...Hugo Herbelin
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-08-15More self-contained code for tclWITHHOLES.Pierre-Marie Pédrot
2014-07-13Adding a "time" tactical for benchmarking purposes. In case the tacticHugo Herbelin
2014-07-10check_for_interrupt: better (but slower) in threading modeEnrico Tassi
2014-07-07Revert "time tac" (committed by mistake).Hugo Herbelin
2014-07-07time tacHugo Herbelin
2014-06-24Clenvtac.clenv_refine in the new monad. Not satisfactory though, because itPierre-Marie Pédrot
2014-06-23Removing opens to Clenvtac to track its use more easily.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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 02:24:19 +0000