| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-16 | Fix lifting in foo_with_full_binders for (co)fixpoints | Gaëtan Gilbert | |
| 2018-11-16 | Small simplification in fold_constr_with_binders | Gaëtan Gilbert | |
| 2018-11-15 | Make set_typing_flags "smart" | Gaëtan Gilbert | |
| Fix #8609 gares said: I believe it was introduced in de20a45 where the option (part of the summary) is moved to the save env. By setting the summary, you unshare the safe env. Now we do that only if needed. The stm uses `==` on the safe env to detect tactics that alter the env, eg abstract. | |||
| 2018-11-09 | Use arrays of names instead of lists in abstract universe names. | Pierre-Marie Pédrot | |
| There is little point in having a list, as there is virtually no sharing nor expansion of bound universe names. This representation is thus more compact. | |||
| 2018-11-09 | Actually store the bound name information in the abstract universe context. | Pierre-Marie Pédrot | |
| 2018-11-09 | Force the user to provide names when generating abstract universe contexts. | Pierre-Marie Pédrot | |
| For now this data is not stored, but the code checks that indeed the number of names provided coincide with the instance length. I had to reimplement the same kind of workaround hack in section handling as the one already performed in UnivNames because the name information is not present in the section data structure. This deserves a FIXME. | |||
| 2018-11-09 | Adding universe names to polymorphic entry instances. | Pierre-Marie Pédrot | |
| 2018-11-06 | [checker] Refactor by sharing code with the kernel | Maxime Dénès | |
| For historical reasons, the checker was duplicating a lot of code of the kernel. The main differences I found were bug fixes that had not been backported. With this patch, the checker uses the kernel as a library to serve the same purpose as before: validation of a `.vo` file, re-typechecking all definitions a posteriori. We also rename some files from the checker so that they don't clash with kernel files. | |||
| 2018-11-06 | Move debug term printer to kernel | Maxime Dénès | |
| 2018-11-05 | Merge PR #8870: Pass native and VM flags to the kernel through environment | Pierre-Marie Pédrot | |
| 2018-11-05 | Merge PR #8866: Check universe instances in Typing | Pierre-Marie Pédrot | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |