| Commit message (Expand) | Author | Age |
* | Merge PR #6169: Clean up/deprecated options | Maxime Dénès | 2017-12-14 |
|\ |
|
* | | [proof] Embed evar_map in RefinerError exception. | Emilio Jesus Gallego Arias | 2017-12-11 |
| * | Remove deprecated option Tactic Compat Context. | Théo Zimmermann | 2017-12-11 |
|/ |
|
* | Merge PR #6158: Allows a level in the raw and glob printers | Maxime Dénès | 2017-12-08 |
|\ |
|
* | | more complete not-fully-applied error messages, #6145 | Paul Steckler | 2017-11-28 |
| * | Extending further PR#6047 (system to register printers for Ltac values). | Hugo Herbelin | 2017-11-24 |
|/ |
|
* | Adding support for syntax "let _ := e in e'" in Ltac. | Hugo Herbelin | 2017-11-04 |
* | Ltac Debug: exporting env and sigma when needed so that term can be printed. | Hugo Herbelin | 2017-11-02 |
* | Binding ltac printing functions to the system of generic printing. | Hugo Herbelin | 2017-11-02 |
* | Setting a system to register printers for Ltac values. | Hugo Herbelin | 2017-11-02 |
* | [general] Remove Econstr dependency from `intf` | Emilio Jesus Gallego Arias | 2017-10-25 |
* | Merge PR #1078: Report missing arguments in error message | Maxime Dénès | 2017-10-04 |
|\ |
|
* | | Efficient fresh name generation relying on sets. | Pierre-Marie Pédrot | 2017-09-28 |
| * | Report missing arguments in error message | Tej Chajed | 2017-09-21 |
|/ |
|
* | Making detyping potentially lazy. | Pierre-Marie Pédrot | 2017-09-04 |
* | Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name | Maxime Dénès | 2017-08-31 |
|\ |
|
| * | Adapting code to renaming Option.fold_map -> Option.fold_left_map. | Hugo Herbelin | 2017-08-29 |
| * | Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map | Hugo Herbelin | 2017-08-29 |
* | | Move type_uconstr to Tacinterp. | Maxime Dénès | 2017-08-01 |
|/ |
|
* | Removing default evar-normalization for ARGUMENT EXTEND. | Pierre-Marie Pédrot | 2017-07-26 |
* | [api] Remove type equalities from API. | Emilio Jesus Gallego Arias | 2017-07-25 |
* | [API] Remove `open API` in ml files in favor of `-open API` flag. | Emilio Jesus Gallego Arias | 2017-07-17 |
* | Bump year in headers. | Pierre-Marie Pédrot | 2017-07-04 |
* | Merge PR#763: [proof] Deprecate redundant wrappers. | Maxime Dénès | 2017-06-14 |
|\ |
|
* \ | Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match"). | Maxime Dénès | 2017-06-14 |
|\ \ |
|
| | * | [proof] Deprecate redundant wrappers. | Emilio Jesus Gallego Arias | 2017-06-11 |
* | | | Remove (useless) aliases from the API. | Matej Košík | 2017-06-10 |
| |/
|/| |
|
| * | A fix to #5414 (ident bound by ltac names now known for "match"). | Hugo Herbelin | 2017-06-09 |
|/ |
|
* | Put all plugins behind an "API". | Matej Kosik | 2017-06-07 |
* | Remove the Sigma (monotonous state) API. | Maxime Dénès | 2017-06-06 |
* | Merge PR#600: Some factorizations of ltac interpretation functions between ss... | Maxime Dénès | 2017-06-06 |
|\ |
|
* \ | Merge PR#716: Don't double up on periods in anomalies | Maxime Dénès | 2017-06-06 |
|\ \ |
|
* \ \ | Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ... | Maxime Dénès | 2017-06-05 |
|\ \ \ |
|
| | * | | Drop '.' from CErrors.anomaly, insert it in args | Jason Gross | 2017-06-02 |
| |/ /
|/| | |
|
* | | | Merge PR#561: Improving the Name API | Maxime Dénès | 2017-06-01 |
|\ \ \ |
|
| | * | | Renaming allow_patvar flag of intern_gen into pattern_mode. | Hugo Herbelin | 2017-05-31 |
| | | * | Factorizing interp_gen through a function interpreting glob_constr. | Hugo Herbelin | 2017-05-31 |
| | | * | Splitting interp_open_constr into two variants, with or without type classes. | Hugo Herbelin | 2017-05-31 |
| | |/ |
|
| * / | Creating a module Nameops.Name extending module Names.Name. | Hugo Herbelin | 2017-05-31 |
| |/ |
|
* | | Adding "epose", "eset", "eremember" which allow to set terms with | Hugo Herbelin | 2017-05-30 |
* | | Adding "eassert", "eenough", "epose proof", which allow to state | Hugo Herbelin | 2017-05-30 |
|/ |
|
* | Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings | Maxime Dénès | 2017-05-25 |
|\ |
|
* \ | Merge PR#608: Allow Ltac2 as a plugin | Maxime Dénès | 2017-05-25 |
|\ \ |
|
* \ \ | Merge PR#481: [option] Remove support for non-synchronous options. | Maxime Dénès | 2017-05-25 |
|\ \ \ |
|
* \ \ \ | Merge branch 'trunk' into located_switch | Emilio Jesus Gallego Arias | 2017-05-24 |
|\ \ \ \ |
|
| | * | | | [option] Remove support for non-synchronous options. | Emilio Jesus Gallego Arias | 2017-05-24 |
| |/ / / |
|
| | | * | Clarifying the interpretation path for the "constr_with_binding" argument. | Hugo Herbelin | 2017-05-22 |
| | |/
| |/| |
|
| | * | Generalizing the tactic-in-term embedding to any generic argument. | Pierre-Marie Pédrot | 2017-05-03 |
| | * | Allowing to pass arbitrary data in internalization environments. | Pierre-Marie Pédrot | 2017-05-03 |
| |/ |
|
| * | Remove unused [open] statements | Gaetan Gilbert | 2017-04-27 |