aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/tacinterp.ml
Commit message (Expand)AuthorAge
* 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
|\ \
| | * [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
* | | Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
| |/ |/|
| * A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
|/
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Merge PR#600: Some factorizations of ltac interpretation functions between ss...Gravatar Maxime Dénès2017-06-06
|\
* \ Merge PR#716: Don't double up on periods in anomaliesGravatar Maxime Dénès2017-06-06
|\ \
* \ \ Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...Gravatar Maxime Dénès2017-06-05
|\ \ \
| | * | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| |/ / |/| |
* | | Merge PR#561: Improving the Name APIGravatar Maxime Dénès2017-06-01
|\ \ \
| | * | Renaming allow_patvar flag of intern_gen into pattern_mode.Gravatar Hugo Herbelin2017-05-31
| | | * Factorizing interp_gen through a function interpreting glob_constr.Gravatar Hugo Herbelin2017-05-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-25 09:08:59 +0000