aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacticals.ml
AgeCommit message (Expand)Author
2021-03-22Factorize goal selector handlingGaëtan Gilbert
2020-11-26Fixes #13456: regression where tactic exists started to check evars increment...Hugo Herbelin
2020-09-29Adding a few tacticals for the purpose of porting funind to new proof engine.Hugo Herbelin
2020-09-07Refine test for unresolved evars: not reachable from initial evarsMatthieu Sozeau
2020-08-31Move elim-specific code from Tacticals to Elim.Pierre-Marie Pédrot
2020-07-06Primitive persistent arraysMaxime Dénès
2020-06-29Move the FailError exception from Refiner to Tacticals.Pierre-Marie Pédrot
2020-06-29Remove the deprecated functions from refiner, moving them to Tacticals.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-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-05-07Deprecate the legacy tacticals from module Refiner.Pierre-Marie Pédrot
2020-05-03Export missing tacticals.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-06unsafe_type_of -> get_type_of in Elim.general_decomposer + pf_apply in ifOnHypGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Tacticals.elimination_thenGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Tacticals.general_elim_then_usingGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-08-27[cleanup] Replace uses of UserError constructor, clarify exception names.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-29[proofs] Remove unused API [detected by coverage]Emilio Jesus Gallego Arias
2019-05-24Fixing typosJPR
2019-05-23Fixing typos - Part 3JPR
2019-04-10Remove calls to global env from indrecMaxime Dénès
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-21[legacy proof engine] Remove some cruft.Emilio Jesus Gallego Arias
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-09-26[print] Restrict use of "debug" Termops printer.Emilio Jesus Gallego Arias
2018-09-23Checking if low-level name printers are used on purpose or not.Hugo Herbelin
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-06-12[api] Misctypes removal: tactic flags.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-01[api] Move bullets and goals selectors to `proofs/`Emilio Jesus Gallego Arias
2018-04-29Strict focusing using Default Goal Selector.Gaëtan Gilbert
2018-04-29tclSELECT: SelectAll never happensGaëtan Gilbert
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-03-27Adding tacticals tclBINDFIRST/tclBINDLAST.Hugo Herbelin
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-01Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Hugo Herbelin
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-12[engine] Remove ghost parameter from `Proofview.Goal.t`Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:07:37 +0000