aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
AgeCommit message (Expand)Author
2020-10-07Merge PR #13115: Derive Inversion does not allow leftover evarsPierre-Marie Pédrot
2020-10-07Merge PR #13119: Fix retyping anomaly in rewritePierre-Marie Pédrot
2020-10-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ...coqbot-app[bot]
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-09-30Fix retyping anomaly in rewriteGaëtan Gilbert
2020-09-30Further simplification of the typeclass registration API.Pierre-Marie Pédrot
2020-09-30Derive Inversion does not allow leftover evarsGaëtan Gilbert
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-18Merge PR #12963: Formally deprecate the double induction tactic.Hugo Herbelin
2020-09-17[leminv] Use higher-level Declare API.Emilio Jesus Gallego Arias
2020-09-17[leminv] Remove unused catch.Emilio Jesus Gallego Arias
2020-09-17Formally deprecate the double induction tactic.Pierre-Marie Pédrot
2020-09-16More improvements in locating tactic errors.Hugo Herbelin
2020-09-11Adding a wit_natural standard argument.Hugo Herbelin
2020-09-11Turn integer into natural in several mlgsPierre Roux
2020-09-11[refman] Rename int to integerPierre Roux
2020-09-08Merge PR #12993: Remove deprecated tactic cutrewrite.Clément Pit-Claudel
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-09-06Fix printing of `change` tactic, which was printed as `change_no_check` and v...Lasse Blaauwbroek
2020-09-02Abstract type for allowed evarsMaxime Dénès
2020-09-02Replace `frozen` by `allowed` evars in evarconv, and delay themMaxime Dénès
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-07-08[obligations] Functionalize Program stateEmilio Jesus Gallego Arias
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
2020-07-01[state] Consolidate state handling in VernacstateEmilio Jesus Gallego Arias
2020-07-01UIP in SPropGaëtan Gilbert
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-26[declare] Merge remaining obligations bits into DeclareEmilio Jesus Gallego Arias
2020-06-26[declare] Improve organization of proof/constant information.Emilio Jesus Gallego Arias
2020-06-26[declare] Reify Proof.t API into the Proof module.Emilio Jesus Gallego Arias
2020-06-26[declare] Move udecl to Info structure.Emilio Jesus Gallego Arias
2020-06-26[declare] [api] Removal of duplicated type aliases.Emilio Jesus Gallego Arias
2020-06-26[declare] Refactor constant information into a record.Emilio Jesus Gallego Arias
2020-06-26[declare] Remove Lemmas moduleEmilio Jesus Gallego Arias
2020-06-26[declare] Move proof information to declare.Emilio Jesus Gallego Arias
2020-06-24Merge Clenvtac into Clenv.Pierre-Marie Pédrot
2020-06-11Merge PR #12423: Remove info tactic, deprecated in 8.5Pierre-Marie Pédrot
2020-05-30Remove info tactic, deprecated in 8.5Jim Fehrle
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-16Merge PR #11566: [misc] Better preserve backtraces in several modulesPierre-Marie Pédrot
2020-05-15Merge PR #11755: [exn] [tactics] improve backtraces on monadic errorsPierre-Marie Pédrot
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:50:40 +0000