aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/tacinterp.ml
AgeCommit message (Expand)Author
2021-03-22Factorize goal selector handlingGaëtan Gilbert
2021-03-12Move the responsibility of type-checking to the caller for tactic-in-terms.Pierre-Marie Pédrot
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-11-23Merge PR #13417: Use nat_or_var in grammar where negative values don't make s...coqbot-app[bot]
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-20Granting #9816: apply in takes several hypotheses.Hugo Herbelin
2020-10-28Fixes #13241 (nested Ltac functions were wrongly reporting error on the inner...Hugo Herbelin
2020-10-27Rename tactic_expr -> ltac_exprJim Fehrle
2020-10-26Improve tactic interpreter registration API a bitGaëtan Gilbert
2020-10-14Deprecating wit_var to the benefit of its synonymous wit_hyp.Hugo Herbelin
2020-10-09Merge PR #13088: [stm] move par: to comTacticcoqbot-app[bot]
2020-10-09[stm] move par: implementation to vernac/comTactic and stm/partacEnrico Tassi
2020-09-25Merge PR #12999: More improvements in locating tactic errorscoqbot-app[bot]
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-09-16More improvements in locating tactic errors.Hugo Herbelin
2020-09-11Adding a wit_natural standard argument.Hugo Herbelin
2020-08-27tacinterp mini cleanup useless letinGaëtan Gilbert
2020-08-19Yet other tactic error location fixes (see PR#12223 and PR#12774).Hugo Herbelin
2020-08-19Prefer eval_tactic_ist, which has error localisation, to interp_tactic.Hugo Herbelin
2020-08-19In tacinterp.ml, renaming eval_tactic into eval_tactic_ist to match the API.Hugo Herbelin
2020-08-18Remaining bugs in PR#12223 which fixed location of tactic errors (issue #12152).Hugo Herbelin
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-05-30Remove info tactic, deprecated in 8.5Jim Fehrle
2020-05-16Merge PR #11566: [misc] Better preserve backtraces in several modulesPierre-Marie Pédrot
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-05-12Merge PR #12223: Locating error again in atomic tactics (fixes #12152)Pierre-Marie Pédrot
2020-05-11Merge PR #12273: Deprecate Refiner APIEmilio Jesus Gallego Arias
2020-05-10Locating error again in TacAtom and TacAlias (fixes #12152, fixes #12255).Hugo Herbelin
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-07Deprecate the legacy tacticals from module Refiner.Pierre-Marie Pédrot
2020-05-07Export API to recover values out of Ltac application.Pierre-Marie Pédrot
2020-04-15[proof] Merge `Pfedit` into proofs.Emilio Jesus Gallego Arias
2020-03-31Try only using TC for conversion in cominductive (not great but let's see)Gaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2019-11-28Tacinterp: push_trace doesn't need to be wrapped in a tacticGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-06-19Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations i...Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-16Deprecate "intro_pattern" in tactic notations in favor of "simple_intropattern".Hugo Herbelin
2019-05-23Fixing typos - Part 2JPR
2019-04-29Exposing a change_no_check tactic.Hugo Herbelin
2019-03-27[geninterp] Track polymorphic status in tactic interpretation.Emilio Jesus Gallego Arias
2019-03-27[coqpp] [ltac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-12Merge PR #7819: Ho matching occ selEnrico Tassi
2019-02-18Merge PR #9142: Disable Ltac backtracesHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:35:18 +0000