| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-16 | {Univops -> Vars}.universes_of_constr | Gaëtan Gilbert | |
| It's basically an occur check so it makes sense to put it in vars | |||
| 2018-10-16 | UnivGen.extend_context -> Univ.extend_in_context_set | Gaëtan Gilbert | |
| Such a basic function can live in Univ rather than the higher level UnivGen. | |||
| 2018-10-16 | Simplify vars_of_global usage | Gaëtan Gilbert | |
| 2018-10-16 | Simplify fresh_foo_instance functions and pretyping of univ instance | Gaëtan Gilbert | |
| 2018-10-16 | Deprecate Global.universes_of_global (replaced by environ version) | Gaëtan Gilbert | |
| 2018-10-16 | Merge PR #8695: Adding a functional version of constant- and ↵ | Pierre-Marie Pédrot | |
| mind_of_delta_kn + functional version of is_polymorphic | |||
| 2018-10-15 | Correct some spelling errors | Benjamin Barenblat | |
| Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`. | |||
| 2018-10-11 | A state-free version of is_polymorphic. | Hugo Herbelin | |
| 2018-10-11 | Adding a functional version of constant_of_delta_kn. | Hugo Herbelin | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |