aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2020-09-02Remove unused API from Elim.Pierre-Marie Pédrot
2020-08-31Move elim-specific code from Tacticals to Elim.Pierre-Marie Pédrot
2020-08-28Clarify variable names in abstract implementationGaëtan Gilbert
2020-08-28Make abstract compatible with mangle namesGaëtan Gilbert
2020-08-27Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfooPierre-Marie Pédrot
2020-08-26Make future_goals stack explicit in the evarmapMaxime Dénès
2020-08-26Move given_up goals to evar_mapMaxime Dénès
2020-08-26Better encapsulation of future goalsMaxime Dénès
2020-08-25Deprecate intro_usingGaëtan Gilbert
2020-08-25elim.ml: stop using intro_usingGaëtan Gilbert
2020-08-25Make decide equality compatible with mangled names.Gaëtan Gilbert
2020-08-24Merge PR #12565: Dnets now consider axioms as being opaque for pattern recogn...coqbot
2020-08-24Merge PR #12816: Fixes #12787: anomaly of tactic injection in the presence of...Pierre-Marie Pédrot
2020-08-20Use properly fresh names for Scheme EqualityJasper Hugunin
2020-08-20Quick fix to #12787 (injection anomaly due to inconsistent comp. of free vars).Hugo Herbelin
2020-08-20Do not store the transparent state in delayed dnets.Pierre-Marie Pédrot
2020-08-20Dnets now consider axioms as being opaque for pattern recognition.Pierre-Marie Pédrot
2020-08-19Replace Hints.head_constr_bound with Hints.head_bound.Pierre-Marie Pédrot
2020-08-19Simplify the computation of the head global for hint patterns.Pierre-Marie Pédrot
2020-08-19Ensure statically that Hint Extern comes with a pattern.Pierre-Marie Pédrot
2020-08-19Merge PR #12822: Do not precompute hint dnets eagerlyMatthieu Sozeau
2020-08-19Merge PR #12725: Store evar identity instances in evarinfo / named_context_valEnrico Tassi
2020-08-18Rename VM-related kernel/cfoo files to kernel/vmfooGaëtan Gilbert
2020-08-17Merge PR #12841: Recommend replace as a replacement to cutrewrite.coqbot
2020-08-17Recommend replace as a replacement to cutrewrite.Théo Zimmermann
2020-08-17Merge PR #12751: Fixes reduction effect printing in the presence of non purel...Pierre-Marie Pédrot
2020-08-14Do not precompute hint dnets eagerly.Pierre-Marie Pédrot
2020-08-13Merge PR #12720: Factor code related to class hint clenvHugo Herbelin
2020-08-13Merge PR #12718: Do not rely on higher-order interfaces for patterns in dnets.Hugo Herbelin
2020-08-12Cosmetic changes as suggested by SkySkimmer.Pierre-Marie Pédrot
2020-08-12Further code simplification in typeclass resolution tactic.Pierre-Marie Pédrot
2020-08-12Split the uses of connect_hint_clenv into two different functions.Pierre-Marie Pédrot
2020-08-12Tentatively more efficient implementation of e_give_exact for typeclasses.Pierre-Marie Pédrot
2020-08-12Export a dedicated function that applies immediately a hint.Pierre-Marie Pédrot
2020-08-12Code simplification around hint manipulation in Class_tactics.Pierre-Marie Pédrot
2020-08-12Make the Hint.hint type private.Pierre-Marie Pédrot
2020-08-12Move connect_hint_clenv from Auto to Hints.Pierre-Marie Pédrot
2020-08-12Do not do a round trip with auto hint representation in autoapply.Pierre-Marie Pédrot
2020-08-12Do not tamper with hints in Class_tactics.with_prods.Pierre-Marie Pédrot
2020-08-12Perfom an goal enter in the relevant class tactics instead of outside.Pierre-Marie Pédrot
2020-08-12Inline Class_tactics.clenv_of_prods.Pierre-Marie Pédrot
2020-08-10Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746)Cyril Cohen
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
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-27Do not rely on higher-order interfaces for patterns in dnets.Pierre-Marie Pédrot
2020-07-24Fixes reduction effect printing in the presence of non purely applicative sta...Hugo Herbelin
2020-07-22Clarify Global.env usage in ppvernacGaëtan Gilbert
2020-07-09[exn] Remove some uses of printEmilio Jesus Gallego Arias
2020-07-08Remove Evarutil.new_evar_instance from the API.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 15:00:28 +0000