Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #900: [proofs] Remove circular dependency from Proofview to Goal. | 2017-07-20 | |
|\ | |||
* \ | Merge PR #899: [general] Move files to directories so they match linking order. | 2017-07-20 | |
|\ \ | |||
* \ \ | Merge PR #903: Documenting the purity / marshallability invariant of ↵ | 2017-07-20 | |
|\ \ \ | | | | | | | | | | | | | persistent states. | ||
| * | | | Documenting the purity / marshallability invariant of persistent states. | 2017-07-20 | |
| | | | | |||
* | | | | Merge PR #898: [pp] Fix bugs 5651 [incorrect thunk in pretty printer] | 2017-07-20 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #896: Prepare De Bruijn universe abstractions, Spin-off: Checker | 2017-07-20 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #869: Enforce alternating separators in typeclass debug output | 2017-07-20 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #877: Travis+4.05.0 | 2017-07-20 | |
|\ \ \ \ \ \ \ | |_|_|_|/ / / |/| | | | | | | |||
* | | | | | | | Merge branch 'v8.7' | 2017-07-20 | |
|\ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ | Merge PR #745: Add timing scripts | 2017-07-19 | |
| |\ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR #855: Deprecate options that were introduced for compatibility with ↵ | 2017-07-19 | |
| |\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 8.5. | ||
* | \ \ \ \ \ \ \ \ | Merge PR #770: [proof] Move bullets to their own module. | 2017-07-19 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | * | [proofs] Remove circular dependency from Proofview to Goal. | 2017-07-19 | |
| |_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | |||
| | | | | | | | | * | [general] Move files to directories matching linking order. | 2017-07-19 | |
| |_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`, `Miscprint`) to their proper place as they were declared in different `mllib` files than the one in their directory. In some cases this could be refined but we don't do anything fancy, we just reflect the status quo. | ||
* | | | | | | | | | Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag. | 2017-07-19 | |
|\ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | * | [pp] Fix bugs 5651 [incorrect thunk in pretty printer] | 2017-07-19 | |
| |_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | Fix bug introduced by a Haskell programmer. | ||
| | | | | | | | * | Fixing the checker w.r.t. wrongly used abstract universe contexts. | 2017-07-19 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It seems we were not testing the checker on cumulative inductive types, because judging from the code, it would just have exploded in anomalies. Before this patch, the checker was mixing De Bruijn indices with named variables, resulting in ill-formed universe contexts used throughout the checking of cumulative inductive types. This patch also gets rid of a lot of now dead code, and removes abstraction breaking code from the checker. | ||
* | | | | | | | | | Merge PR #895: [ci] VST is now built with IGNORECOQVERSION=true. | 2017-07-19 | |
|\ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ |/| | | | | | | | | |||
| * | | | | | | | | [ci] VST is now built with IGNORECOQVERSION=true. | 2017-07-18 | |
|/ / / / / / / / | |||
* | | | | | | | | Merge PR #781: Remove dead code [Universes.simplify_universe_context] | 2017-07-17 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #783: Remove some useless code in Term_typing | 2017-07-17 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #822: [meta] [api] Fix META file for API introduction. | 2017-07-17 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | | * | | | | | | | [funind] Remove spurious character in comment. | 2017-07-17 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It breaks ocamlmerlin. | ||
| | | | * | | | | | | | [API] Remove `open API` in ml files in favor of `-open API` flag. | 2017-07-17 | |
| | | | | | | | | | | | |||
| | | | * | | | | | | | [meta] [api] Fix META file for API introduction. | 2017-07-17 | |
| |_|_|/ / / / / / / |/| | | | | | | | | | |||
* | | | | | | | | | | Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers | 2017-07-17 | |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #881: Adapting base_include to 91df40272 (body_of_constant_body ↵ | 2017-07-17 | |
|\ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | moved to Global). | ||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #879: Adding debug printers related to universes | 2017-07-17 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #874: Adding econstr printer to "include" file. | 2017-07-17 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #872: [travis] Display info on tested commit for PR builds. | 2017-07-17 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #865: RefMan-ext: fix some typos | 2017-07-17 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #862: Adding support for bindings tags to explicit prefix/suffix ↵ | 2017-07-17 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | rather than colors | ||
| | | | | | | | | | | | * \ \ \ \ | Merge PR #861: Fix typo in documentation for identity | 2017-07-17 | |
| | | | | | | | | | | | |\ \ \ \ \ | |||
| | | | | | * | | | | | | | | | | | | Adapting to 91df40272 (body_of_constant_body moved to global). | 2017-07-16 | |
| |_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | |||
| | * | | | | | | | | | | | | | | | Update with non structurally recursive | 2017-07-14 | |
| | | | | | | | | | | | | | | | | | |||
| | | | | * | | | | | | | | | | | | Adding debug printers related to universes in the default debugger source file. | 2017-07-14 | |
| |_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | |||
| | | | | * | | | | | | | | | | | Fix a typo in dev/changes. | 2017-07-14 | |
| | | | | | | | | | | | | | | | | |||
| | | | | * | | | | | | | | | | | Document the changes in API brought by this series of patches. | 2017-07-14 | |
| | | | | | | | | | | | | | | | | |||
| | | | | * | | | | | | | | | | | Getting rid of abstraction breaking code in tclABSTRACT. | 2017-07-14 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is probably the hardest case of them all, because tclABSTRACT fundamentally relies on the names of universes from the constant instance being the same as the one in the current goal. Adding to that the fact that the kernel is doing strange things when provided with a polymorphic definition with body universe constraints, it turns out to be a hellish nightmare to handle properly. At some point we need to clarifiy this in the kernel as well, although we leave it for some other patch. | ||
| | | | | | | | | | | | | | * | | [travis] Update testing to 4.05.0 + Camlp5 7.01 | 2017-07-13 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | |||
| | | | | * | | | | | | | | | | Removing a use of AUContext.instance in the STM. | 2017-07-13 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We only delay monomorphic proofs in quick mode, so that their universe context will always be empty. | ||
| | | | | * | | | | | | | | | | Removing the uses of abstraction-breaking code in Lemmas. | 2017-07-13 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I had to slightly tweak a test in order to work around a bug of simpl that loses universes constraints when refolding polymorphic fixpoints. | ||
| | | | | | | | | | * | | | | | Set version to 8.7+alpha. | 2017-07-13 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It is a valid git tag (unlike 8.7~alpha) and will be considered by most tools as < 8.7.0 (unlike 8.7.0+alpha). | ||
| | | | | * | | | | | | | | | | Removing the uses of abstraction-breaking code in Obligations. | 2017-07-13 | |
| | | | | | | | | | | | | | | | |||
| | | | | * | | | | | | | | | | Remove the function Global.type_of_global_unsafe. | 2017-07-13 | |
| | | | | | | | | | | | | | | | |||
| | | | | * | | | | | | | | | | The only abstraction-breaking function in Univ is now AUContext.instance. | 2017-07-13 | |
| | | | | | | | | | | | | | | | |||
| | | | | * | | | | | | | | | | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global. | 2017-07-13 | |
| | | | | | | | | | | | | | | | |||
| | | | | * | | | | | | | | | | Getting rid of AUContext abstraction breakers in Elimschemes. | 2017-07-13 | |
| | | | | | | | | | | | | | | | |||
| | | | | * | | | | | | | | | | Getting rid of AUContext abstraction breakers in Discharge. | 2017-07-13 | |
| | | | | | | | | | | | | | | | |||
| | | | | * | | | | | | | | | | Make the typeclass implementation fully compatible with universe polymorphism. | 2017-07-13 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This essentially means storing the abstract universe context in the typeclass data, and abstracting it when necessary. |