aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2020-06-05Merge PR #12336: Factorize code in hint declaration.Hugo 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
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
2020-05-25Remove the prolog tactic.Pierre-Marie Pédrot
2020-05-19Delay evaluating arguments of the "exists" tacticAttila Gáspár
2020-05-16Factorize code in hint declaration.Pierre-Marie Pédrot
2020-05-15Search: new clauses for searching head, conclusion, kind...Hugo Herbelin
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
2020-05-12Merge PR #12146: Fixes #10812: tactic subst failure with section variables in...Pierre-Marie Pédrot
2020-05-11Merge PR #12273: Deprecate Refiner APIEmilio Jesus Gallego Arias
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
2020-05-09Add another note about removing a tactic after abstractJason Gross
2020-05-09Revert "[with_strategy] Fix for coqchk"Jason Gross
2020-05-09[with_strategy] Fix for coqchkJason Gross
2020-05-09Fix a bug with with_strategy, behavior on multisuccess tacticsJason Gross
2020-05-09Fix the `with_strategy` tactic to work with `abstract`Jason Gross
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-07Deprecate the legacy tacticals from module Refiner.Pierre-Marie Pédrot
2020-05-07Tactic subst now inactive on section variables occurring indirectly in goal.Hugo Herbelin
2020-05-03Export missing tacticals.Pierre-Marie Pédrot
2020-05-03Wrap Refiner.refiner in the tactic monad.Pierre-Marie Pédrot
2020-04-29Merge the call to tclEFFECTS into find_scheme.Pierre-Marie Pédrot
2020-04-28Return an option in lookup_scheme.Pierre-Marie Pédrot
2020-04-28Stop relying on side-effects for recursive scheme declaration.Pierre-Marie Pédrot
2020-04-23Merge PR #12130: [declare] [tactics] Move declare to `vernac`Pierre-Marie Pédrot
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
2020-04-21Merge PR #12116: Fixing #12045: missing normalization in conclusion of custom...Pierre-Marie Pédrot
2020-04-21Merge PR #11883: Fix #7812: autounfold's behavior depends on file namesHugo Herbelin
2020-04-21[declare] [tactics] Move declare to `vernac`Emilio Jesus Gallego Arias
2020-04-21[hints] Move and split Hint Declaration AST to vernacEmilio Jesus Gallego Arias
2020-04-20Fixing #12045 (missing normalization in conclusion of custom induction scheme).Hugo Herbelin
2020-04-15[tmp] Compat API for CIEmilio Jesus Gallego Arias
2020-04-15[declare] Rename `Declare.t` to `Declare.Proof.t`Emilio Jesus Gallego Arias
2020-04-15[proof] Move functions related to `Proof.t` to `Proof`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Pfedit` into proofs.Emilio Jesus Gallego Arias
2020-04-15[proofs] Move pfedit to `proofs`Emilio Jesus Gallego Arias
2020-04-15[declare] [abstract] Do evars check in declare_abstractEmilio Jesus Gallego Arias
2020-04-15[declare] Mark APIs as scheduled for removal; remove a couple.Emilio Jesus Gallego Arias
2020-04-15[proof] [abstract] Move internal declaration code to `Declare`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-04-15[proof] Move proof_global functionality to Proof_global from PfeditEmilio Jesus Gallego Arias
2020-04-14Merge PR #11820: Partial importsMaxime Dénès
2020-04-13correctly open objects for Names filtersGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:26:39 +0000