aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
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.
2020-06-16Code simplification in Autorewrite.Pierre-Marie Pédrot
2020-06-16Remove dead code in autorewrite.Pierre-Marie Pédrot
2020-06-06Fix #12442: Confusing error message when the intro pattern of "apply in" failsAttila Gáspár
2020-06-05Merge PR #12336: Factorize code in hint declaration.Hugo Herbelin
Reviewed-by: herbelin
2020-06-04Move the Cbn module to tactics/.Pierre-Marie Pédrot
2020-06-04Move the cbn reduction to its own file, and simplify the RAKAM accordingly.Pierre-Marie Pédrot
2020-06-02Enforce statically the invariant that a goal comes with its database in eauto.Pierre-Marie Pédrot
2020-06-02Simplify Eauto.e_trivial_resolve.Pierre-Marie Pédrot
No need to create various mapping of lists when a filter would suffice.
2020-06-02Factor the computation of head constant in Eauto resolution.Pierre-Marie Pédrot
2020-06-02Make explicit the computation of lists of goals in eauto.Pierre-Marie Pédrot
2020-06-02Some wrapper cleanup around eauto.Pierre-Marie Pédrot
2020-05-28Merge PR #12399: Remove the prolog tactic.Théo Zimmermann
Reviewed-by: Zimmi48
2020-05-25Remove the prolog tactic.Pierre-Marie Pédrot
It was deprecated in 8.12 and not used in the wild.
2020-05-19Delay evaluating arguments of the "exists" tacticAttila Gáspár
2020-05-16Factorize code in hint declaration.Pierre-Marie Pédrot
This allows to remove internal API from the mli as well.
2020-05-15Search: new clauses for searching head, conclusion, kind...Hugo Herbelin
- new clauses "hyp:", "concl:", "headhyp:" and "headconcl:" to restrict match to an hypothesis or the conclusion, possibly only at the head (like SearchHead in this latter case) - new clause "is:" to search by kind of object (for some list of kinds) - support for any combination of negations, disjunctions and conjunctions, using a syntax close to that of intropatterns.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:32:29 +0000