| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-30 | Merge PR #9068: [dune] Minor tweak of dependencies. | Théo Zimmermann | |
| 2018-11-27 | Fix #8364: making univ algebraic when already equal to another. | Gaëtan Gilbert | |
| When making a universe a variable we iterate through the universes we're equal to and if we find one we update the substitution accordingly. NB: The bug called make_flexible_variable on Top.15 and ~~~ {Top.15 Top.14} |= Top.11 < Top.6 Top.14 < Top.5 Top.11 = Top.15 ALGEBRAIC UNIVERSES:{Top.17 Top.16} UNDEFINED UNIVERSES:Top.17 := Top.14+1 Top.16 := Top.14+1 WEAK CONSTRAINTS: ~~~ so now we would add [Top.15 := Top.11]. | |||
| 2018-11-27 | Merge PR #8850: Private universes for opaque polymorphic constants. | Matthieu Sozeau | |
| 2018-11-27 | Merge PR #8255: Fast typing of application nodes | Maxime Dénès | |
| 2018-11-26 | [dune] Minor tweak of dependencies. | Emilio Jesus Gallego Arias | |
| `clib` doesn't need `dynlink`, but `lib` does, similarly for `threads`, `num`... We align Dune and META deps. | |||
| 2018-11-26 | Put -indices-matter in typing_flags | Gaëtan Gilbert | |
| 2018-11-24 | Merge PR #8929: Fix fixpoint related lifting in open recursors + related ↵ | Pierre-Marie Pédrot | |
| cleanups | |||
| 2018-11-23 | Merge PR #8995: Don't redeclare constraints of fields in Include | Maxime Dénès | |
| 2018-11-23 | Local universes for opaque polymorphic constants. | Gaëtan Gilbert | |
| 2018-11-20 | Add a check that the return stack of an FProd is indeed empty. | Pierre-Marie Pédrot | |
| 2018-11-20 | Use a closure for the domain argument of FProd. | Pierre-Marie Pédrot | |
| The use of a term is not needed for the fast typing algorithm of the application case, so this tweak brings the best of both worlds. | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |