aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.ml
AgeCommit message (Expand)Author
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
2020-05-09Revert "[with_strategy] Fix for coqchk"Jason Gross
2020-05-09[with_strategy] Fix for coqchkJason Gross
2020-05-09Fix a bug with with_strategy, behavior on multisuccess tacticsJason Gross
2020-05-09Fix the `with_strategy` tactic to work with `abstract`Jason Gross
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-03Wrap Refiner.refiner in the tactic monad.Pierre-Marie Pédrot
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
2020-04-20Fixing #12045 (missing normalization in conclusion of custom induction scheme).Hugo Herbelin
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
2020-03-31Try only using TC for conversion in cominductive (not great but let's see)Gaëtan Gilbert
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-13Replacing catchable_exception by noncritical in try-with blocks.Hugo Herbelin
2020-03-06Merge PR #11723: Fix mishandling of sigma in guess_elim (regression from 8.11)Pierre-Marie Pédrot
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-03-02Refine patch for clearer scoping of evar_mapMatthieu Sozeau
2020-03-01Fix mishandling of sigma in guess_elim (regression from 8.11)Matthieu Sozeau
2020-02-13Merge PR #11521: Remove Goptions.opt_name fieldPierre-Marie Pédrot
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-12Standardize constr -> globref operations to use destRef/isRef/isRefXGaëtan Gilbert
2020-02-06Remove Clenv.mk_clenv_type_of (hidden unsafe_type_of)Gaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.prove_transitivityGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 04:40:56 +0000