aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.ml
AgeCommit message (Expand)Author
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
2020-02-06unsafe_type_of -> type_of in Tactics.symmetry_inGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.induction_gen_l + fix bad envGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Tactics.is_functional_inductionGaëtan Gilbert
2020-02-06Fix evar map leak in Tactics.find_induction_typeGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.given_elimGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.guess_elimGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.abstract_argsGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Tactics.atomize_param_of_ind_thenGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.rewrite_hyp_then (+ tclEVARSTHEN)Gaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.intro_or_and_patternGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.intro_decomp_eq (hipattern changes)Gaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.cut_and_applyGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.find_eliminatorGaëtan Gilbert
2020-02-06unsafe_type_of + match -> sort_of in Tactics.cutGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.change_on_subtermGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.convert_conclGaëtan Gilbert
2020-01-12fix #11279. Specialize h no longer expands letins in the type of h.Pierre Courtieu
2019-12-10Fixing #9893 (Letins not supported in the specialized hypothesis).Pierre Courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 03:45:57 +0000