aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)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
We inline the clenv universe refreshing, since it was the only place in the code that used it. Furthermore it was performing useless substitutions in the clenv.
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
It was unnecessarily obfuscated.
2020-08-10Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746)Cyril Cohen
Reviewed-by: CohenCyril Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: maximedenes Ack-by: ppedrot
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
The old API was taking a function to decompose constr patterns into dnet patterns, but it was applying it in an eager way. So there is not point in exposing such a complex interface. Instead, we make explicit the dnet pattern type, export a function that turns a constr pattern into a dnet pattern, and make the add and remove dnet functions take a dnet pattern instead. This only affects pattern-consuming functions. The lookup function, which operates on kernel terms instead of constr patterns, is still relying on HO primitives.
2020-07-24Fixes reduction effect printing in the presence of non purely applicative ↵Hugo Herbelin
stacks.
2020-07-22Clarify Global.env usage in ppvernacGaëtan Gilbert
2020-07-09[exn] Remove some uses of printEmilio Jesus Gallego Arias
Exceptions should not printed except for the top-level. There is the weird anomaly-absorbing code in `Reductionops`, I wonder how frequent that case is, but as the exception is absorbed printing there could have a real impact.
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
Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot Ack-by: proux01 Ack-by: silene
2020-07-06Primitive persistent arraysMaxime Dénès
Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-07-06Merge PR #12622: Use goal cycling instead of manual evar generation order in ↵Gaëtan Gilbert
internal_cut_rev Reviewed-by: SkySkimmer
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes
2020-07-02Merge PR #12572: Correctly classify variables as being unfoldable in dnet ↵Gaëtan Gilbert
patterns. Reviewed-by: SkySkimmer Reviewed-by: maximedenes
2020-07-01Use goal cycling instead of manual evar generation order in internal_cut_rev.Pierre-Marie Pédrot
This reduces the combinatorial complexity of the function, and the code size as well.
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-30Merge PR #12599: Remove the Refiner moduleEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-29Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_listPierre-Marie Pédrot
Reviewed-by: ppedrot
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
Reviewed-by: ejgallego
2020-06-24Remove the catchable-exception related functions.Pierre-Marie Pédrot
They were deprecated in 8.12.
2020-06-24Merge Clenvtac into Clenv.Pierre-Marie Pédrot
Having two different modules led to the availability of internal API in the mli.
2020-06-24Remove all uses of clenv_unique_resolver.Pierre-Marie Pédrot
All calls to this function are now factorized through Clenvtac.res_pf.
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
Fixes #12571.
2020-06-23Use the unification result for eauto's eapply.Pierre-Marie Pédrot
Instead of dropping the unification result and calling simple eapply with the original term, we simply use the same code path as auto and typeclass eauto, i.e. reuse the clenv for refinement.
2020-06-22Merge PR #12520: Cleanup the autorewrite implementationHugo Herbelin
Reviewed-by: herbelin
2020-06-19Move the hint polymorphic status to the hint instance.Pierre-Marie Pédrot
It is only used for this kind of hints, never for Extern / Unfold.
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
The only use was seemingly a bug introduced in 0aec9033a by an accidental variable capture. There is indeed no reason that the set of variables of a hint corresponds to the one of the current environment.
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
They are always the same.
2020-06-19Do not be verbose when declaring subclass hints.Pierre-Marie Pédrot
There is no point in warning about eauto being the only one able to use those hints, since they will be used by typeclass_eauto instead. It was probably an oversight introduced quite a long time ago.
2020-06-19Factorize hint flags in Class_tatcis.make_make_resolve_hyp.Pierre-Marie Pédrot
They were always instantiated with the triple (true, false, false).
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
This is barely more meaningful but at least we do not rely on an antiquated API now.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 13:19:45 +0000