aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/tacinterp.ml
AgeCommit message (Expand)Author
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
2017-12-14Make [abstract] nodes show up in the Ltac profileJason Gross
2017-12-14Merge PR #6386: Catch errors while coercing 'and' intro patternsMaxime Dénès
2017-12-14Merge PR #6169: Clean up/deprecated optionsMaxime Dénès
2017-12-12Fix #5081 by more fine-grained LtacProf recordingJason Gross
2017-12-11Catch errors while coercing 'and' intro patternsTej Chajed
2017-12-11[proof] Embed evar_map in RefinerError exception.Emilio Jesus Gallego Arias
2017-12-11Remove deprecated option Tactic Compat Context.Théo Zimmermann
2017-12-08Merge PR #6158: Allows a level in the raw and glob printersMaxime Dénès
2017-11-28more complete not-fully-applied error messages, #6145Paul Steckler
2017-11-24Extending further PR#6047 (system to register printers for Ltac values).Hugo Herbelin
2017-11-04Adding support for syntax "let _ := e in e'" in Ltac.Hugo Herbelin
2017-11-02Ltac Debug: exporting env and sigma when needed so that term can be printed.Hugo Herbelin
2017-11-02Binding ltac printing functions to the system of generic printing.Hugo Herbelin
2017-11-02Setting a system to register printers for Ltac values.Hugo Herbelin
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
2017-10-04Merge PR #1078: Report missing arguments in error messageMaxime Dénès
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-09-21Report missing arguments in error messageTej Chajed
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-08-31Merge PR #980: Adding combinators + a canonical renaming in List, Option, NameMaxime Dénès
2017-08-29Adapting code to renaming Option.fold_map -> Option.fold_left_map.Hugo Herbelin
2017-08-29Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapHugo Herbelin
2017-08-01Move type_uconstr to Tacinterp.Maxime Dénès
2017-07-26Removing default evar-normalization for ARGUMENT EXTEND.Pierre-Marie Pédrot
2017-07-25[api] Remove type equalities from API.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#763: [proof] Deprecate redundant wrappers.Maxime Dénès
2017-06-14Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 22:11:44 +0000