aboutsummaryrefslogtreecommitdiff
path: root/tactics/class_tactics.ml
AgeCommit message (Expand)Author
2021-01-11Use the Evarutil cache for Class_tactics.evar_dependencies.Pierre-Marie Pédrot
2020-11-04Further API cleanup after the removal of forward hints.Pierre-Marie Pédrot
2020-09-30Remove the forward class hint feature.Pierre-Marie Pédrot
2020-09-13Statically ensure that only polymophic hint terms come with a context.Pierre-Marie Pédrot
2020-09-02Abstract type for allowed evarsMaxime Dénès
2020-09-02Replace `frozen` by `allowed` evars in evarconv, and delay themMaxime Dénès
2020-09-01Unify the shelvesMaxime Dénès
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-20Dnets now consider axioms as being opaque for pattern recognition.Pierre-Marie Pédrot
2020-08-19Ensure statically that Hint Extern comes with a pattern.Pierre-Marie Pédrot
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-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-07-09[exn] Remove some uses of printEmilio Jesus Gallego Arias
2020-06-29Move the FailError exception from Refiner to Tacticals.Pierre-Marie Pédrot
2020-06-25Merge PR #12579: Simplify Clenv APIEmilio Jesus Gallego Arias
2020-06-24Remove the catchable-exception related functions.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-19Move the hint polymorphic status to the hint instance.Pierre-Marie Pédrot
2020-06-19Wrap the content of full hints into a record.Pierre-Marie Pédrot
2020-06-19Remove access to hint section variables.Pierre-Marie Pédrot
2020-06-19Opacify the type of hint metadata.Pierre-Marie Pédrot
2020-06-19Do not export flags in Hints.make_resolves.Pierre-Marie Pédrot
2020-06-19Do not be verbose when declaring subclass hints.Pierre-Marie Pédrot
2020-06-19Factorize hint flags in Class_tatcis.make_make_resolve_hyp.Pierre-Marie Pédrot
2020-05-16Factorize code in hint declaration.Pierre-Marie Pédrot
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
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-13Implementing postponed constraints in TC resolutionMatthieu Sozeau
2020-03-13Fixing a non-protected try-with in class_tactics.ml.Hugo Herbelin
2020-03-13Removing catchable_exception test in tclOR/tclORELSE.Hugo Herbelin
2020-03-05Merge PR #7791: Deprecating the declaration of arbitrary terms as hints.Maxime Dénès
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-02-28Deprecate the OCaml API to declare term Hints.Pierre-Marie Pédrot
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Class_tactics.autoapplyGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:08:50 +0000