| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-11 | The cbv reduction does not rely on the kernel info data structure anymore. | Pierre-Marie Pédrot | |
| 2018-10-08 | Merge PR #8654: Remove FCast from CClosure.fterm. | Maxime Dénès | |
| 2018-10-06 | [api] Remove (most) 8.9 deprecated objects. | Emilio Jesus Gallego Arias | |
| A few of them will be of help for future cleanups. We have spared the stuff in `Names` due to bad organization of this module following the split from `Term`, which really difficult things removing the constructors. | |||
| 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-10-04 | Remove FCast from CClosure.fterm. | Pierre-Marie Pédrot | |
| Just like in the Sixth Sense, it turns out it was dead code all along. | |||
| 2018-10-02 | Merge PR #8572: [config] Miscellaneous cleaning of configuration variables. | Pierre-Marie Pédrot | |
| 2018-10-02 | Merge PR #7522: [ocaml] Update required OCaml version to 4.05.0 | Pierre-Marie Pédrot | |
| 2018-10-01 | Merge PR #8254: Inline the definition of CClosure.mk_clos_deep. | Maxime Dénès | |
| 2018-10-01 | Merge PR #8577: Generalize type of compare_head_with functions, and use for ↵ | Pierre-Marie Pédrot | |
| econstr | |||
| 2018-10-01 | Merge PR #8575: Remove {Safe_typing,Global}.push_context | Maxime Dénès | |
| 2018-10-01 | [nit] Qualify `Envars` use. | Emilio Jesus Gallego Arias | |
| This eases grep to implement a different location system. | |||
| 2018-09-28 | Generalize type of compare_head_with functions | Gaëtan Gilbert | |
| 2018-09-27 | [dune] [merlin] Fix some usability issues. | Emilio Jesus Gallego Arias | |
| As suggested on Gitter by @maximedenes we improve documentation and update Kernel's `.merlin` so it actually reports on the stricter set of warnings. We also set the language version to the proper one so users will get a better error message [the fact that we can use `(env_var ...)` with the wrong Dune version is a Dune bug indeed]. | |||
| 2018-09-27 | Remove {Safe_typing,Global}.push_context | Gaëtan Gilbert | |
| Adding a ucontext to the global environment only makes sense internally when checking a polymorphic constant. | |||
| 2018-09-27 | Merge PR #8475: Centralize the reliance on abstract universe context internals | Gaëtan Gilbert | |
| 2018-09-26 | [ocaml] Update required OCaml version to 4.05.0 | Emilio Jesus Gallego Arias | |
| Closes #7380. Ubuntu 18.04 and Debian Buster will ship this OCaml version so it makes sense we bump our dependency to 4.05.0 as we can use some newer compiler features. | |||
| 2018-09-26 | Inline the definition of CClosure.mk_clos_deep. | Pierre-Marie Pédrot | |
| An important part of this function was dead code, due to the fact it was only used for whd evaluation of specific shapes of constr. | |||
| 2018-09-26 | Merge PR #8534: Checking if low-level name printers are used on purpose or not | Maxime Dénès | |
| 2018-09-24 | [kernel] Compile with almost all warnings enabled. | Emilio Jesus Gallego Arias | |
| This is a partial resurrection of #6423 but only for the kernel. IMHO, we pay a bit of price for this but it is a good safety measure. Only warning "4: fragile pattern matching" and "44: open hides a type" are disabled. We would like to enable 44 for sure once we do some alias cleanup. | |||
| 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-21 | Remove hash based univ level compare | Gaëtan Gilbert | |
| 2018-09-21 | Fix printing of abstract universe contexts. | Pierre-Marie Pédrot | |
| Due to their representation using names, the instance was not properly displayed. | |||
| 2018-09-19 | Merge PR #8341: Reduce universe redeclarations (catching AlreadyDeclared) | Matthieu Sozeau | |
| 2018-09-19 | Merge PR #8447: Cleaning in the retroknowledge | Pierre-Marie Pédrot | |
| 2018-09-17 | Merge PR #6906: [VM] Optimize structured values | Pierre-Marie Pédrot | |
| 2018-09-17 | Merge PR #8053: [dune] Add apidoc target using `odoc` | Gaëtan Gilbert | |
| 2018-09-17 | OCaml now exports the min and max non-constant tags, let's use it | Maxime Dénès | |
| 2018-09-17 | Add assertion on tags in eq_structured_constants | Maxime Dénès | |
| 2018-09-17 | [VM] Allocate a bit less in digits_from_uint | Maxime Dénès | |
| 2018-09-17 | [VM] Inject structured constants in values without reallocating them. | Maxime Dénès | |
| 2018-09-17 | [VM] Move structured_constant to Vmvalues | Maxime Dénès | |
| 2018-09-14 | Register: simpler syntax | Vincent Laporte | |
| 2018-09-14 | Retroknowledge: use GlobRef.t instead of Constr.t as entry | Vincent Laporte | |
| 2018-09-14 | Retroknowledge: simpler parsing rules | Vincent Laporte | |
| 2018-09-14 | Retroknowledge: remove the (unused) by clause | Vincent Laporte | |
| 2018-09-14 | Retroknowledge.KInt31: remove the (unused) group parameter | Vincent Laporte | |
| 2018-09-13 | Merge PR #8434: Canonical representation of kernel substitutions | Maxime Dénès | |
| 2018-09-13 | Merge PR #8436: Move maps & sets indexed by GlobRef.t into the kernel | Maxime Dénès | |
| 2018-09-13 | Do not catch already declared universes in Environ.add_universes | Gaëtan Gilbert | |
| Include is still causing repeat declarations in add_universes_set | |||
| 2018-09-13 | Avoid repeat univ declaration in cumulative subtyping check | Gaëtan Gilbert | |
| 2018-09-13 | Avoid repeat universe declarations for constants with split univs | Gaëtan Gilbert | |
| 2018-09-13 | Kernel: fully obey mind_entry_template | Gaëtan Gilbert | |
| 2018-09-12 | Fix mli-doc following #7109. | Théo Zimmermann | |
| 2018-09-12 | Move maps & sets indexed by GlobRef.t into the kernel | Vincent Laporte | |
| 2018-09-12 | Merge PR #8097: Use more efficient accu check for cofix unfolding in native ↵ | Maxime Dénès | |
| compilation. | |||
| 2018-09-12 | Merge PR #7109: Term combinators respecting the canonical structure of ↵ | Maxime Dénès | |
| branches and return predicate | |||
| 2018-09-11 | Merge PR #8278: Do not inline let-bound functions in clambda optimization. | Maxime Dénès | |
| 2018-09-10 | [dune] Add apidoc target using `odoc` | Emilio Jesus Gallego Arias | |
| We build the `@doc` target in the `dune` job: - The documentation can be found in `_build/default/_doc/` - We had to fix a couple of quoting problems. | |||
| 2018-09-07 | Canonical representation of kernel substitutions. | Pierre-Marie Pédrot | |
| For some reason the code was implementing substitutions as pairs of maps, but the invariant ensured actually no observable difference between fetching a module ident from one or the other. The split seems to be mostly due to historical reasons. We make this invariant static by representing substitutions as a single map. | |||
| 2018-09-07 | Remove dead code in Mod_subst. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |