| Age | Commit message (Expand) | Author |
|---|
| 2017-12-14 | Make [abstract] nodes show up in the Ltac profile | Jason Gross |
| 2017-12-14 | Merge PR #6386: Catch errors while coercing 'and' intro patterns | Maxime Dénès |
| 2017-12-14 | Merge PR #6169: Clean up/deprecated options | Maxime Dénès |
| 2017-12-12 | Fix #5081 by more fine-grained LtacProf recording | Jason Gross |
| 2017-12-11 | Catch errors while coercing 'and' intro patterns | Tej Chajed |
| 2017-12-11 | [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-08 | Merge PR #6158: Allows a level in the raw and glob printers | Maxime Dénès |
| 2017-11-28 | more complete not-fully-applied error messages, #6145 | Paul Steckler |
| 2017-11-24 | Extending further PR#6047 (system to register printers for Ltac values). | Hugo Herbelin |
| 2017-11-04 | Adding support for syntax "let _ := e in e'" in Ltac. | Hugo Herbelin |
| 2017-11-02 | 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-10-25 | [general] Remove Econstr dependency from `intf` | Emilio Jesus Gallego Arias |
| 2017-10-04 | Merge PR #1078: Report missing arguments in error message | Maxime Dénès |
| 2017-09-28 | Efficient fresh name generation relying on sets. | Pierre-Marie Pédrot |
| 2017-09-21 | Report missing arguments in error message | Tej Chajed |
| 2017-09-04 | Making detyping potentially lazy. | Pierre-Marie Pédrot |
| 2017-08-31 | Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name | Maxime Dénès |
| 2017-08-29 | 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-01 | Move type_uconstr to Tacinterp. | Maxime Dénès |
| 2017-07-26 | Removing 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-04 | Bump year in headers. | Pierre-Marie Pédrot |
| 2017-06-14 | 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-11 | [proof] Deprecate redundant wrappers. | Emilio Jesus Gallego Arias |
| 2017-06-10 | Remove (useless) aliases from the API. | Matej Košík |
| 2017-06-09 | A fix to #5414 (ident bound by ltac names now known for "match"). | Hugo Herbelin |
| 2017-06-07 | Put all plugins behind an "API". | Matej Kosik |
| 2017-06-06 | 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-05 | Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ... | Maxime Dénès |
| 2017-06-02 | Drop '.' from CErrors.anomaly, insert it in args | Jason Gross |
| 2017-06-01 | Merge PR#561: Improving the Name API | Maxime Dénès |
| 2017-05-31 | 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-30 | 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-25 | 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-24 | Merge branch 'trunk' into located_switch | Emilio Jesus Gallego Arias |
| 2017-05-24 | [option] Remove support for non-synchronous options. | Emilio Jesus Gallego Arias |
