| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-10 | [Canonical structures] “not_canonical” annotation to field declarations | Vincent Laporte | |
| 2019-05-10 | [Canonical structures] Some projections may not be canonical | Vincent Laporte | |
| 2019-05-07 | [Canonical structures] Deforestation | Vincent Laporte | |
| 2019-04-10 | Remove calls to Global.env and Libobject from Recordops | Maxime Dénès | |
| 2019-04-01 | Merge PR #9870: Minor refactoring in canonical structures | Enrico Tassi | |
| Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: ppedrot | |||
| 2019-03-30 | Error when [foo.(bar)] is used with nonprojection [bar] | Gaëtan Gilbert | |
| (warn if bar is a nonprimitive projection) | |||
| 2019-03-30 | [Canonical structures] Minor refactoring | Vincent Laporte | |
| 2019-03-30 | [Canonical structures] Minor cleaning | Vincent Laporte | |
| 2019-01-24 | Simplify code for Recordops.cs_pattern_of_constr | Gaëtan Gilbert | |
| This has different behaviour if called on an applied Rel, not sure if that ever happens. | |||
| 2019-01-22 | [CS] recognize applied primitive projections as keys (fix #9375) | Enrico Tassi | |
| 2018-12-12 | Merge PR #8974: Fix mod_subst wrt universe polymorphism | Maxime Dénès | |
| 2018-12-09 | [doc] Enable Warning 50 [incorrect doc comment] and fix comments. | Emilio Jesus Gallego Arias | |
| This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :) | |||
| 2018-12-05 | Fix mod_subst wrt universe polymorphism | Gaëtan Gilbert | |
| 2018-11-16 | No Projection.constant in projection <-> constant declaration | Gaëtan Gilbert | |
| Enabled by previous commit about Heads. | |||
| 2018-11-06 | Move debug term printer to kernel | Maxime Dénès | |
| 2018-10-18 | [api] Qualify access to `Nametab` | Emilio Jesus Gallego Arias | |
| In general, `Nametab` is not a module you want to open globally as it exposes very generic identifiers such as `push` or `global`. Thus, we remove all global opens and qualify `Nametab` access. The patch is small and confirms the hypothesis that `Nametab` access happens in few places thus it doesn't need a global open. It is also very convenient to be able to use `grep` to see accesses to the namespace table. | |||
| 2018-10-14 | Parameterizing default inhabitant for impossible cases with an environment. | Hugo Herbelin | |
| 2018-10-05 | [kernel] Remove section paths from `KerName.t` | Maxime Dénès | |
| We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code. Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not. | |||
| 2018-09-26 | [print] Restrict use of "debug" Termops printer. | Emilio Jesus Gallego Arias | |
| The functions in `Termops.print_*` are meant to be debug printers, however, they are sometimes used in non-debug code due to a API confusion. We thus wrap such functions into an `Internal` module, improve documentation, and switch users to the right API. | |||
| 2018-09-23 | Checking if low-level name printers are used on purpose or not. | Hugo Herbelin | |
| In particular we check if really used for internal debugging purpose or to display a message to the user. In the latter case, we replace it (when possible) by a higher-level printer (e.g. printing foo instead of Top.foo). In the former case, we clarify that the use is a debugging use. Still not perfect (see a few FIXME). | |||
| 2018-09-12 | Move maps & sets indexed by GlobRef.t into the kernel | Vincent Laporte | |
| 2018-07-24 | Projections use index representation | Gaëtan Gilbert | |
| The upper layers still need a mapping constant -> projection, which is provided by Recordops. | |||
| 2018-05-25 | Remove some occurrences of Evd.empty | Maxime Dénès | |
| We address the easy ones, but they should probably be all removed. | |||
| 2018-05-23 | Moving Option.smart_map to Option.Smart.map. | Hugo Herbelin | |
| 2018-05-23 | Collecting List.smart_* functions into a module List.Smart. | Hugo Herbelin | |
| 2018-05-04 | [api] Rename `global_reference` to `GlobRef.t` to follow kernel style. | Emilio Jesus Gallego Arias | |
| In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at. | |||
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann | |
| 2018-02-06 | More detailed error messages for Canonical Structure, #6398 | Paul Steckler | |
| 2017-11-22 | [api] Deprecate Term destructors, move to Constr | Emilio Jesus Gallego Arias | |
| We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`. | |||
| 2017-11-13 | [api] Another large deprecation, `Nameops` | Emilio Jesus Gallego Arias | |
| 2017-11-06 | [api] Move structures deprecated in the API to the core. | Emilio Jesus Gallego Arias | |
| We do up to `Term` which is the main bulk of the changes. | |||
| 2017-11-06 | [api] Deprecate all legacy uses of Names in core. | Emilio Jesus Gallego Arias | |
| This will allow to merge back `Names` with `API.Names` | |||
| 2017-10-17 | unification: fix BZ#5692, recognize prim projs as CS projections | Matthieu Sozeau | |
| 2017-10-17 | Properly handling projection parameters in canonical structures. | Pierre-Marie Pédrot | |
| 2017-10-17 | Handling primitive projections in canonical structures. | Pierre-Marie Pédrot | |
| 2017-07-13 | Getting rid of AUContext abstraction breakers in Recordops. | Pierre-Marie Pédrot | |
| 2017-07-13 | Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel | Maxime Dénès | |
| 2017-07-11 | Safe API for accessing universe constraints of global references. | Pierre-Marie Pédrot | |
| Instead of returning either an instance or the set of constraints, we rather return the corresponding abstracted context. We also push back all uses of abstraction-breaking calls from these functions out of the kernel. | |||
| 2017-07-07 | Merge PR #863: Fixing environment in warning "Projection value has no head ↵ | Maxime Dénès | |
| constant". | |||
| 2017-07-07 | Fixing environment in warning "Projection value has no head constant". | Hugo Herbelin | |
| Delaying also some computation needed for printing to the time of really printing it. | |||
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2017-06-16 | Clean up universes of constants and inductives | Amin Timany | |
| 2017-02-14 | Ltac now uses evar-based constrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Reductionops now return EConstrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Inv API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Recordops API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Reductionops API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Termops API using EConstr. | Pierre-Marie Pédrot | |
| 2016-08-19 | Make the user_err header an optional parameter. | Emilio Jesus Gallego Arias | |
| Suggested by @ppedrot | |||
| 2016-08-19 | Remove errorlabstrm in favor of user_err | Emilio Jesus Gallego Arias | |
| As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |