aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2020-07-08Remove Evarutil.new_evar_from_context from the API.Pierre-Marie Pédrot
2020-07-06Merge PR #11604: Primitive persistent arraysPierre-Marie Pédrot
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-06Merge PR #12622: Use goal cycling instead of manual evar generation order in ...Gaëtan Gilbert
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
2020-07-02Merge PR #12572: Correctly classify variables as being unfoldable in dnet pat...Gaëtan Gilbert
2020-07-01Use goal cycling instead of manual evar generation order in internal_cut_rev.Pierre-Marie Pédrot
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-30Merge PR #12599: Remove the Refiner moduleEmilio Jesus Gallego Arias
2020-06-29Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_listPierre-Marie Pédrot
2020-06-29Move the FailError exception from Refiner to Tacticals.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-29Remove the deprecated functions from refiner, moving them 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-24Remove dead code in branch_args.Pierre-Marie Pédrot
2020-06-23Correctly classify variables as being unfoldable in dnet patterns.Pierre-Marie Pédrot
2020-06-23Use the unification result for eauto's eapply.Pierre-Marie Pédrot
2020-06-22Merge PR #12520: Cleanup the autorewrite implementationHugo Herbelin
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-19Remove dead code in the Hints API.Pierre-Marie Pédrot
2020-06-19Do not export Hints.make_extern.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-06-18Fix #12228 negative integers not accepted in ltac integer_listPierre Roux
2020-06-16Use evar clauses instead of meta clauses in Autorewrite hint registration.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:36:51 +0000