aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/tacinterp.ml
AgeCommit message (Expand)Author
2019-02-12[tactics] Remove dependency of abstract on global proof state.Emilio Jesus Gallego Arias
2019-02-08locus: Add an AtLeastOneOccurrence constructor.Matthieu Sozeau
2019-02-05Unset the Ltac backtrace printing by default.Pierre-Marie Pédrot
2019-02-05Add an option not to register Ltac backtraces.Pierre-Marie Pédrot
2019-02-05Make Program a regular attributeMaxime Dénès
2018-12-22Merge PR #9248: Fix #7904: update proofview env after ltac constr:()Pierre-Marie Pédrot
2018-12-19Fix #7904: update proofview env after ltac constr:()Gaëtan Gilbert
2018-12-19Merge PR #9139: [engine] Allow debug printers to access the environment.Pierre-Marie Pédrot
2018-12-14[proof] Rework proof interface.Emilio Jesus Gallego Arias
2018-12-13[engine] Allow debug printers to access the environment.Emilio Jesus Gallego Arias
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-12-04Document undocumented flags and optionsJim Fehrle
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-11-17[ltac] Use CAst nodes in the tactic AST.Emilio Jesus Gallego Arias
2018-11-16Remove the implicit tactic feature following #7229.Pierre-Marie Pédrot
2018-11-03Merge PR #8844: Move abstract out of tactics.mlPierre-Marie Pédrot
2018-10-31Merge PR #8759: Fix #8755: Uncaught exception Ltac_plugin.Taccoerce.CannotCoe...Hugo Herbelin
2018-10-30Remove fully_empty_glob_sign which uses a dummy environmentMaxime Dénès
2018-10-30Move abstract out of tactics.mlGaëtan Gilbert
2018-10-19Fix #8755: Uncaught exception Ltac_plugin.Taccoerce.CannotCoerceTo.Pierre-Marie Pédrot
2018-10-18[api] Qualify access to `Nametab`Emilio Jesus Gallego Arias
2018-09-27Fixes #8553 (regression of tactic "change" under binders).Hugo Herbelin
2018-09-26Merge PR #8534: Checking if low-level name printers are used on purpose or notMaxime Dénès
2018-09-24[engine] Remove and deprecate `nf_enter` et al.Emilio Jesus Gallego Arias
2018-09-23[api] Deprecate constructors of deprecated datatypes.Emilio Jesus Gallego Arias
2018-09-23Checking if low-level name printers are used on purpose or not.Hugo Herbelin
2018-09-19Merge PR #8246: Implementing an internal basic version of the "pose" tactic i...Enrico Tassi
2018-09-10Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.Hugo Herbelin
2018-08-13Less crazy implementation of the "pose" family of tactics.Pierre-Marie Pédrot
2018-07-20Merge PR #8037: Export a function to apply toplevel tactic values in Tacinterp.Enrico Tassi
2018-07-12Tactic deprecation machineryMaxime Dénès
2018-07-10Export a function to apply toplevel tactic values in Tacinterp.Pierre-Marie Pédrot
2018-07-03Taccoerce: remove various unused arguments.Gaëtan Gilbert
2018-06-18Remove reference name type.Maxime Dénès
2018-06-14Workaround to handle non-value arguments in tactics.Cyprien Mangin
2018-06-12[api] Remove Misctypes.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-14Deprecate Typing.e_* functionsGaëtan Gilbert
2018-04-13Making tactic-in-term aware of "Set Ltac Debug".Hugo Herbelin
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-08Make most of TACTIC EXTEND macros runtime calls.Maxime Dénès
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2017-12-22Remove legacy Value.normalize function.Maxime Dénès
2017-12-18Merge PR #6406: Make [abstract] nodes show up in the Ltac profileMaxime Dénès
2017-12-18Merge PR #6411: Fix #5081 by more fine-grained LtacProf recordingMaxime Dénès
2017-12-14Pass a ghost location for abstractJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:02:52 +0000