aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/tactic_debug.ml
AgeCommit message (Expand)Author
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-13Removing catchable_exception test in tclOR/tclORELSE.Hugo Herbelin
2020-03-03[exn] Keep information from multiple extra exn handlersEmilio Jesus Gallego Arias
2020-02-24[exn] remove `raise` taking optional exception information argumentEmilio Jesus Gallego Arias
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-07-07[error] Remove special error printing pre-processingEmilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-03-27[coqpp] [ltac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
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-09-26[print] Restrict use of "debug" Termops printer.Emilio Jesus Gallego Arias
2018-09-24[engine] Remove and deprecate `nf_enter` et al.Emilio Jesus Gallego Arias
2018-04-12Merge PR #7107: Fixes #7100: lost of main file location in case of Ltac failu...Pierre-Marie Pédrot
2018-04-04Fixing #7100 (lost of main file location in case of Ltac failure in other file).Hugo Herbelin
2018-04-02Fix #6404 - Print tactics called by ML tacticsJason Gross
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-14Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Maxime Dénès
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-09A fix to #5414 (ident bound by ltac names now known for "match").Hugo Herbelin
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-05-25Merge PR#481: [option] Remove support for non-synchronous options.Maxime Dénès
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-05-04Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in bat...Hugo Herbelin
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-15Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:32:58 +0000