| Age | Commit message (Expand) | Author |
|---|
| 2020-09-08 | Merge PR #12993: Remove deprecated tactic cutrewrite. | Clément Pit-Claudel |
| 2020-09-08 | Remove deprecated tactic cutrewrite. | Théo Zimmermann |
| 2020-09-06 | Fix printing of `change` tactic, which was printed as `change_no_check` and v... | Lasse Blaauwbroek |
| 2020-09-02 | Abstract type for allowed evars | Maxime Dénès |
| 2020-09-02 | Replace `frozen` by `allowed` evars in evarconv, and delay them | Maxime Dénès |
| 2020-08-27 | tacinterp mini cleanup useless letin | Gaëtan Gilbert |
| 2020-08-19 | Yet other tactic error location fixes (see PR#12223 and PR#12774). | Hugo Herbelin |
| 2020-08-19 | Prefer eval_tactic_ist, which has error localisation, to interp_tactic. | Hugo Herbelin |
| 2020-08-19 | In tacinterp.ml, renaming eval_tactic into eval_tactic_ist to match the API. | Hugo Herbelin |
| 2020-08-18 | Remaining bugs in PR#12223 which fixed location of tactic errors (issue #12152). | Hugo Herbelin |
| 2020-07-08 | [obligations] Functionalize Program state | Emilio Jesus Gallego Arias |
| 2020-07-03 | Merge PR #10390: UIP in SProp | Maxime Dénès |
| 2020-07-01 | [state] Consolidate state handling in Vernacstate | Emilio Jesus Gallego Arias |
| 2020-07-01 | UIP in SProp | Gaëtan Gilbert |
| 2020-06-29 | Move the FailError exception from Refiner to Tacticals. | Pierre-Marie Pédrot |
| 2020-06-29 | Remove the deprecated functions from refiner, moving them to Tacticals. | Pierre-Marie Pédrot |
| 2020-06-26 | [declare] Merge remaining obligations bits into Declare | Emilio 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 module | Emilio Jesus Gallego Arias |
| 2020-06-26 | [declare] Move proof information to declare. | Emilio Jesus Gallego Arias |
| 2020-06-24 | Merge Clenvtac into Clenv. | Pierre-Marie Pédrot |
| 2020-06-11 | Merge PR #12423: Remove info tactic, deprecated in 8.5 | Pierre-Marie Pédrot |
| 2020-05-30 | Remove info tactic, deprecated in 8.5 | Jim Fehrle |
| 2020-05-28 | Merge PR #12399: Remove the prolog tactic. | Théo Zimmermann |
| 2020-05-25 | Remove the prolog tactic. | Pierre-Marie Pédrot |
| 2020-05-19 | Delay evaluating arguments of the "exists" tactic | Attila Gáspár |
| 2020-05-16 | Merge PR #11566: [misc] Better preserve backtraces in several modules | Pierre-Marie Pédrot |
| 2020-05-15 | Merge PR #11755: [exn] [tactics] improve backtraces on monadic errors | Pierre-Marie Pédrot |
| 2020-05-15 | [misc] Better preserve backtraces in several modules | Emilio Jesus Gallego Arias |
| 2020-05-14 | Merge PR #12256: Move the static check of evaluability in unfold tactic to ru... | Hugo Herbelin |
| 2020-05-14 | [exn] [tactics] improve backtraces on monadic errors | Emilio Jesus Gallego Arias |
| 2020-05-14 | Merge PR #11922: No more local reduction functions in Reductionops. | Maxime Dénès |
| 2020-05-14 | Tweak the error message of reference internalization. | Pierre-Marie Pédrot |
| 2020-05-14 | Generalize the interpretation of syntactic notation as reference to their head. | Pierre-Marie Pédrot |
| 2020-05-14 | Move the static check of evaluability in unfold tactic to runtime. | Pierre-Marie Pédrot |
| 2020-05-13 | Merge PR #12229: Hopefully consensual cleaning of keywords | Théo Zimmermann |
| 2020-05-12 | Merge PR #12223: Locating error again in atomic tactics (fixes #12152) | Pierre-Marie Pédrot |
| 2020-05-11 | Merge PR #12254: In non-strict mode, accept any variable as a tactic reference. | Hugo Herbelin |
| 2020-05-11 | Merge PR #12273: Deprecate Refiner API | Emilio Jesus Gallego Arias |
| 2020-05-11 | Merge PR #12129: Add a `with_strategy` tactic | Pierre-Marie Pédrot |
| 2020-05-10 | No more local reduction functions in Reductionops. | Pierre-Marie Pédrot |
| 2020-05-10 | Locating error again in TacAtom and TacAlias (fixes #12152, fixes #12255). | Hugo Herbelin |
| 2020-05-09 | Merge PR #12241: [declare] Merge DeclareDef into Declare | Gaëtan Gilbert |
| 2020-05-09 | Add a `with_strategy` tactic | Jason Gross |
| 2020-05-08 | In non-strict mode, accept any variable as a tactic reference. | Pierre-Marie Pédrot |
| 2020-05-07 | [declare] Merge DeclareDef into Declare | Emilio Jesus Gallego Arias |
