| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-20 | More efficient implementation of type_of_apply. | Pierre-Marie Pédrot | |
| 2018-11-20 | Do not wrap FProd return types in a closure. | Pierre-Marie Pédrot | |
| There is little point to this as the type is dependent on an open value and is never computed further. | |||
| 2018-11-20 | Merge PR #7925: Clean transparent state | Maxime Dénès | |
| 2018-11-19 | Merge PR #8894: Print full binders in subtyping incompatible polymorphism error. | Pierre-Marie Pédrot | |
| 2018-11-19 | Rename TranspState into TransparentState. | Pierre-Marie Pédrot | |
| 2018-11-19 | Proper record type and accessors for transparent states. | Pierre-Marie Pédrot | |
| This is documented in dev/doc/changes.md. | |||
| 2018-11-19 | Move transparent_state to its own module. | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #8451: Print Universes Subgraph | Pierre-Marie Pédrot | |
| 2018-11-16 | Use universe names when printing to dot. | Gaëtan Gilbert | |
| 2018-11-16 | Make UGraph printing independent of hash order | Gaëtan Gilbert | |
| 2018-11-16 | We improve a little bit in printing universe constraints signature mismatch. | Hugo Herbelin | |
| Use of boxes to ensure locality of formatting + use of a prlist_with_sep so that there are breaking points only inbetween the elements and not at the end of the list. | |||
| 2018-11-16 | Print full binders in subtyping incompatible polymorphism error. | Gaëtan Gilbert | |
| Close #8891 | |||
| 2018-11-16 | Don't redeclare constraints of fields in Include | Gaëtan Gilbert | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |