| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-05 | Merge PR #8824: Do not check convertibility of pattern types in the kernel | Maxime Dénès | |
| 2018-11-05 | Pass native and VM flags to the kernel through environment | Maxime Dénès | |
| The kernel no longer has to read the configure flag, its value can now be overriden by a coqtop/coqc argument, and more generally is easier to set from a toplevel (such as the checker). We also add a `-bytecode-compiler` flag. Fixes #4607 | |||
| 2018-10-31 | Use standard combinator for Global.set_strategy | Maxime Dénès | |
| 2018-10-31 | Introduce Safe_typing.set_share_reduction | Maxime Dénès | |
| 2018-10-31 | Seeing Global purely as a wrapper on top of kernel functions. | Hugo Herbelin | |
| 2018-10-31 | Merge PR #8752: Enable fragile pattern warning in cclosure | Maxime Dénès | |
| 2018-10-30 | Remove Environ.set_universes / Typing.enrich_env | Gaëtan Gilbert | |
| Made possible by the previous commit passing ~evars to check_hyps_inclusion. | |||
| 2018-10-30 | Check univ instances in Typing. | Gaëtan Gilbert | |
| 2018-10-30 | Simplify universe handling in environ constant_type functions | Gaëtan Gilbert | |
| 2018-10-29 | Do not compare the type arguments in pattern-match branches. | Pierre-Marie Pédrot | |
| We know that the two are living in a common type, so that it is useless to perform the comparison check. Note that we only use this fast-path when the branches are only made of lambda-abstractions, but this covers all actual cases. | |||
| 2018-10-29 | Do not box fconstr closures in pattern-match branches. | Pierre-Marie Pédrot | |
| They are only used once, thus it is completely useless to reallocate arrays that are going to be destructed immediately. | |||
| 2018-10-29 | Integrate convert_shape into convert_stack. | Pierre-Marie Pédrot | |
| No reason to split the code, this function is only used once. | |||
| 2018-10-29 | Merge PR #8780: Cleanup comparing projections through their constants. | Maxime Dénès | |
| 2018-10-26 | Merge PR #8684: Remove a few circumvolutions around parameters of inductive ↵ | Gaëtan Gilbert | |
| entries | |||
| 2018-10-26 | Merge PR #8687: Mini reorganization type of global constr of global | Pierre-Marie Pédrot | |
| 2018-10-26 | Merge PR #8814: Comment Environ.set_universes | Maxime Dénès | |
| 2018-10-26 | Remove a few circumvolutions around parameters of inductive entries | Maxime Dénès | |
| 2018-10-26 | Merge PR #8777: Move side-effects into Safe_typing | Maxime Dénès | |
| 2018-10-26 | Merge PR #8707: Separate cache representation between CClosure and CBV | Maxime Dénès | |
| 2018-10-26 | Merge PR #7186: Moving `fold_constr_with_full_binders` to a place | Maxime Dénès | |
| 2018-10-24 | Comment Environ.set_universes | Gaëtan Gilbert | |
| I looked for this information and forgot about it a couple times so let's put it in writing. | |||
| 2018-10-22 | Merge PR #8708: Stupid but critical unfolding heuristic. | Maxime Dénès | |
| 2018-10-20 | Cleanup comparing projections through their constants. | Gaëtan Gilbert | |
| 2018-10-19 | Moving Global.constr_of_global_in_context to Typeops. | Hugo Herbelin | |
| It is purely functional, so no need for it to be in global now that GlobRef.t are in the kernel. | |||
| 2018-10-19 | Moving Global.type_of_global_in_context to Typeops. | Hugo Herbelin | |
| It is purely functional, so no need for it to be in global now that GlobRef.t are in the kernel. Also updated the comments. | |||
| 2018-10-19 | Cleaning layout typeops.mli. | Hugo Herbelin | |
| 2018-10-19 | Explicitly merge contexts in side-effect universe handling. | Pierre-Marie Pédrot | |
| Instead of threading the universe state and making it grow, we make clear in the signature that the differed side-effects generate constraints to be added. | |||
| 2018-10-19 | Move side-effect typing into Safe_env. | Pierre-Marie Pédrot | |
| This reduces the attack surface of the API, as actually there is only a back and forth between the two modules, and side-effects validity certificates are intuitively nothing more than safe environments. | |||
| 2018-10-17 | Enable fragile pattern warning in cclosure | Gaëtan Gilbert | |
| This file is already mostly in the required style so I wanted to see what it looks like. For a couple matches I locally disabled the warning as it was too annoying otherwise (`when` clauses are especially annoying). There are a couple places where I think it clearly looks better (eg assoc_defined at the beginning of the file) but overall I'm not all that convinced. What do other people think? | |||
| 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-12 | Moving local copy fold_constr_with_full_binders in assumptions.ml to constr.ml. | Hugo Herbelin | |
| This is to move a standard combinator to the place it belongs to. An alternative could have been to put it in termops.ml, but termops.ml is now about econstr, so, even if it makes the kernel "bigger", constr.ml seems to be the best place for this combinator. After all, this combinator is canonical. | |||
| 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-11 | Clean up CClosure code. | Pierre-Marie Pédrot | |
| We take advantage of the separation of implementation from CBV to remove constant code. | |||
| 2018-10-11 | The cbv reduction does not rely on the kernel info data structure anymore. | Pierre-Marie Pédrot | |
| 2018-10-11 | Stupid but critical unfolding heuristic. | Pierre-Marie Pédrot | |
| We favour unfolding of variables over constants because it is more frequent for the former to depend on the latter. This has huge consequences on a few extremely slow lines in mathcomp, up to dividing by 3 single-line invocations that were taking about 30s on my laptop before the patch. | |||
| 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 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |