aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/tacinterp.ml
Commit message (Expand)AuthorAge
* Merge PR #8037: Export a function to apply toplevel tactic values in Tacinterp.Gravatar Enrico Tassi2018-07-20
|\
* | Tactic deprecation machineryGravatar Maxime Dénès2018-07-12
| * Export a function to apply toplevel tactic values in Tacinterp.Gravatar Pierre-Marie Pédrot2018-07-10
|/
* Taccoerce: remove various unused arguments.Gravatar Gaëtan Gilbert2018-07-03
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* Workaround to handle non-value arguments in tactics.Gravatar Cyprien Mangin2018-06-14
* [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* Deprecate Typing.e_* functionsGravatar Gaëtan Gilbert2018-05-14
* Making tactic-in-term aware of "Set Ltac Debug".Gravatar Hugo Herbelin2018-04-13
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* Make most of TACTIC EXTEND macros runtime calls.Gravatar Maxime Dénès2018-03-08
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* Remove legacy Value.normalize function.Gravatar Maxime Dénès2017-12-22
* Merge PR #6406: Make [abstract] nodes show up in the Ltac profileGravatar Maxime Dénès2017-12-18
|\
* \ Merge PR #6411: Fix #5081 by more fine-grained LtacProf recordingGravatar Maxime Dénès2017-12-18
|\ \
| | * Pass a ghost location for abstractGravatar Jason Gross2017-12-14
| | * Make [abstract] nodes show up in the Ltac profileGravatar Jason Gross2017-12-14
| |/ |/|
* | Merge PR #6386: Catch errors while coercing 'and' intro patternsGravatar Maxime Dénès2017-12-14
|\ \
* \ \ Merge PR #6169: Clean up/deprecated optionsGravatar Maxime Dénès2017-12-14
|\ \ \
| | | * Fix #5081 by more fine-grained LtacProf recordingGravatar Jason Gross2017-12-12
| | * | Catch errors while coercing 'and' intro patternsGravatar Tej Chajed2017-12-11
| | |/
* | / [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
| |/ |/|
| * Remove deprecated option Tactic Compat Context.Gravatar Théo Zimmermann2017-12-11
|/
* Merge PR #6158: Allows a level in the raw and glob printersGravatar Maxime Dénès2017-12-08
|\
* | more complete not-fully-applied error messages, #6145Gravatar Paul Steckler2017-11-28
| * Extending further PR#6047 (system to register printers for Ltac values).Gravatar Hugo Herbelin2017-11-24
|/
* Adding support for syntax "let _ := e in e'" in Ltac.Gravatar Hugo Herbelin2017-11-04
* Ltac Debug: exporting env and sigma when needed so that term can be printed.Gravatar Hugo Herbelin2017-11-02
* Binding ltac printing functions to the system of generic printing.Gravatar Hugo Herbelin2017-11-02
* Setting a system to register printers for Ltac values.Gravatar Hugo Herbelin2017-11-02
* [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
* Merge PR #1078: Report missing arguments in error messageGravatar Maxime Dénès2017-10-04
|\
* | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
| * Report missing arguments in error messageGravatar Tej Chajed2017-09-21
|/
* Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
* Merge PR #980: Adding combinators + a canonical renaming in List, Option, NameGravatar Maxime Dénès2017-08-31
|\
| * Adapting code to renaming Option.fold_map -> Option.fold_left_map.Gravatar Hugo Herbelin2017-08-29
| * Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapGravatar Hugo Herbelin2017-08-29
* | Move type_uconstr to Tacinterp.Gravatar Maxime Dénès2017-08-01
|/
* Removing default evar-normalization for ARGUMENT EXTEND.Gravatar Pierre-Marie Pédrot2017-07-26
* [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge PR#763: [proof] Deprecate redundant wrappers.Gravatar Maxime Dénès2017-06-14
|\
* \ Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 20:04:41 +0000