aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.ml
AgeCommit message (Expand)Author
2021-03-30[flags] [profile] Remove bit-rotten CProfile code.Emilio Jesus Gallego Arias
2021-03-26[recordops] complete API rewrite; the module is now called [structures]Enrico Tassi
2021-03-12Further simplification of the term replacing code.Pierre-Marie Pédrot
2021-03-12Algorithmically faster algorithm for term replacing.Pierre-Marie Pédrot
2021-01-22Merge PR #13761: Remove convert_concl_no_check (deprecated in 8.11)Pierre-Marie Pédrot
2021-01-20Merge PR #13721: Remove strong reduction wrapperscoqbot-app[bot]
2021-01-19Remove convert_concl_no_checkJim Fehrle
2021-01-18Preventing internal temporary names to impact the "?H"-like intro-pattern names.Hugo Herbelin
2021-01-18Further simplifications in intro_patterns machinery.Hugo Herbelin
2021-01-18Small reworking of code in intros-pattern.Hugo Herbelin
2021-01-18Fixes #13413: freshness issue with "%" introduction pattern.Hugo Herbelin
2021-01-18Move the two only calls to the strong combinator to their calling site.Pierre-Marie Pédrot
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-12-18Merge PR #13628: Cache meta instances in Clenvcoqbot-app[bot]
2020-12-15Merge PR #13609: Extrude the computation of redexp flags in reduce.coqbot-app[bot]
2020-12-14Make the clenv type private and provide a creation function.Pierre-Marie Pédrot
2020-12-13Removing unused internal introduction-patterns flag assert_style.Hugo Herbelin
2020-12-13Removing flag "Bracketing Last Introduction Pattern".Hugo Herbelin
2020-12-12Small API encapsulation inside Redexpr.Pierre-Marie Pédrot
2020-12-12Extrude the computation of redexp flags in reduce.Pierre-Marie Pédrot
2020-11-26Fixes #13456: regression where tactic exists started to check evars increment...Hugo Herbelin
2020-11-20Granting #9816: apply in takes several hypotheses.Hugo Herbelin
2020-11-16Avoid exposing an internal names when "intros _ H" fails.Hugo Herbelin
2020-10-21Deprecate the non-qualified equality functions on kerpairs.Pierre-Marie Pédrot
2020-09-10Add a fast-path to Tactics.e_change_in_hyps.Pierre-Marie Pédrot
2020-09-09Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable fro...Pierre-Marie Pédrot
2020-09-08Merge PR #12954: Fixes a freshness issue with destruct/induction (see comment...Pierre-Marie Pédrot
2020-09-07Refine test for unresolved evars: not reachable from initial evarsMatthieu Sozeau
2020-09-03Merge PR #12973: Random cleanup around the data structures used in EqualityHugo Herbelin
2020-09-02Do not look for a quantified inductive type in intropattern injection.Pierre-Marie Pédrot
2020-08-31Fix mangle names issue in inductionGaëtan Gilbert
2020-08-31Fixes a freshness issue with induction (see comment in #12944).Hugo Herbelin
2020-08-31Move elim-specific code from Tacticals to Elim.Pierre-Marie Pédrot
2020-08-25Deprecate intro_usingGaëtan Gilbert
2020-08-20Use properly fresh names for Scheme EqualityJasper Hugunin
2020-08-06Actually use the default instance stored inside named_context_val.Pierre-Marie Pédrot
2020-08-06Remove several calls to Evarutil.new_pure_evar.Pierre-Marie Pédrot
2020-07-08Remove Evarutil.new_evar_instance from the API.Pierre-Marie Pédrot
2020-07-08Remove Evarutil.new_evar_from_context from the API.Pierre-Marie Pédrot
2020-07-01Use goal cycling instead of manual evar generation order in internal_cut_rev.Pierre-Marie Pédrot
2020-06-29Moving the remaining Refiner functions to Tacmach.Pierre-Marie Pédrot
2020-06-29Remove Refiner.refiner.Pierre-Marie Pédrot
2020-06-24Merge Clenvtac into Clenv.Pierre-Marie Pédrot
2020-06-24Remove all uses of clenv_unique_resolver.Pierre-Marie Pédrot
2020-06-06Fix #12442: Confusing error message when the intro pattern of "apply in" failsAttila Gáspár
2020-05-19Delay evaluating arguments of the "exists" tacticAttila Gáspár
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
2020-05-09Add another note about removing a tactic after abstractJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:08:47 +0000