| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-12-12 | checker: check inductive types by roundtrip through the kernel. | Gaëtan Gilbert | |
| 2018-12-12 | Merge PR #8974: Fix mod_subst wrt universe polymorphism | Maxime Dénès | |
| 2018-12-12 | Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix ↵ | Maxime Dénès | |
| comments. | |||
| 2018-12-09 | [doc] Enable Warning 50 [incorrect doc comment] and fix comments. | Emilio Jesus Gallego Arias | |
| This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :) | |||
| 2018-12-06 | Revise API for global universes. | Gaëtan Gilbert | |
| Rename Univ.Level.{Qualid -> UGlobal}, remove Univ.Level.Id. Remove the ability to split the argument of `Univ.Level.Level` into a dirpath*int pair (except by going through string hacks like detyping/pretyping(/funind) does). Id.of_string_soft to turn unnamed universes into qualid is pushed up to detyping. (TODO some followup PR clean up more) This makes it pointless to have an opaque type for ints in Univ.Level: it would only be used as argument to Univ.Level.UGlobal.make, ie ~~~ open Univ.Level let x = UGlobal.make dp (Id.make n) (* vs *) let x = UGlobal.make dp n ~~~ Remaining places which create levels from ints are various hacks (eg the dummy in inductive.ml, the Type.n universes in ugraph sort_universes) and univgen. UnivGen does have an opaque type for ints used as univ ids since they get manipulated by the stm. NB: build breaks due to ocamldep issue if UGlobal is named Global instead. | |||
| 2018-12-06 | Fix race condition triggered by fresh universe generation | Maxime Dénès | |
| Remote counters were trying to build universe levels (as opposed to simple integers), but did not have access to the right dirpath at construction time. We fix it by constructing the level only at use time, and we introduce some abstractions for qualified and unqualified level names. | |||
| 2018-12-05 | Fix mod_subst wrt universe polymorphism | Gaëtan Gilbert | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |