aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-07-19Fixing the checker w.r.t. wrongly used abstract universe contexts.Pierre-Marie Pédrot
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.
2017-07-17Merge PR #781: Remove dead code [Universes.simplify_universe_context]Maxime Dénès
2017-07-17Merge PR #783: Remove some useless code in Term_typingMaxime Dénès
2017-07-17Merge PR #822: [meta] [api] Fix META file for API introduction.Maxime Dénès
2017-07-17Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layersMaxime Dénès
2017-07-17Merge PR #881: Adapting base_include to 91df40272 (body_of_constant_body ↵Maxime Dénès
moved to Global).
2017-07-17Merge PR #879: Adding debug printers related to universesMaxime Dénès
2017-07-17Merge PR #874: Adding econstr printer to "include" file.Maxime Dénès
2017-07-17Merge PR #872: [travis] Display info on tested commit for PR builds.Maxime Dénès
2017-07-17Merge PR #865: RefMan-ext: fix some typosMaxime Dénès
2017-07-17Merge PR #862: Adding support for bindings tags to explicit prefix/suffix ↵Maxime Dénès
rather than colors
2017-07-16Adapting to 91df40272 (body_of_constant_body moved to global).Hugo Herbelin
2017-07-14Update with non structurally recursivewilliam-lawvere
2017-07-14Adding debug printers related to universes in the default debugger source file.Pierre-Marie Pédrot
2017-07-14Fix a typo in dev/changes.Pierre-Marie Pédrot
2017-07-14Document the changes in API brought by this series of patches.Pierre-Marie Pédrot
2017-07-14Getting rid of abstraction breaking code in tclABSTRACT.Pierre-Marie Pédrot
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.
2017-07-13Removing a use of AUContext.instance in the STM.Pierre-Marie Pédrot
We only delay monomorphic proofs in quick mode, so that their universe context will always be empty.
2017-07-13Removing the uses of abstraction-breaking code in Lemmas.Pierre-Marie Pédrot
I had to slightly tweak a test in order to work around a bug of simpl that loses universes constraints when refolding polymorphic fixpoints.
2017-07-13Removing the uses of abstraction-breaking code in Obligations.Pierre-Marie Pédrot
2017-07-13Remove the function Global.type_of_global_unsafe.Pierre-Marie Pédrot
2017-07-13The only abstraction-breaking function in Univ is now AUContext.instance.Pierre-Marie Pédrot
2017-07-13Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Pierre-Marie Pédrot
2017-07-13Getting rid of AUContext abstraction breakers in Elimschemes.Pierre-Marie Pédrot
2017-07-13Getting rid of AUContext abstraction breakers in Discharge.Pierre-Marie Pédrot
2017-07-13Make the typeclass implementation fully compatible with universe polymorphism.Pierre-Marie Pédrot
This essentially means storing the abstract universe context in the typeclass data, and abstracting it when necessary.
2017-07-13Safer API for Global.body_of_constant and variants.Pierre-Marie Pédrot
We aditionally return the abstract universe context inside the option. This is relatively painless as most uses were using the option as a boolean.
2017-07-13Safer API for Global.type_of_global_in_context.Pierre-Marie Pédrot
We return the abstract context instead of an arbitrary instantiation.
2017-07-13Getting rid of AUContext abstraction breakers in Record.Pierre-Marie Pédrot
2017-07-13Getting rid of AUContext abstraction breakers in Search.Pierre-Marie Pédrot
2017-07-13Getting rid of AUContext abstraction breakers in Recordops.Pierre-Marie Pédrot
2017-07-13Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: KernelMaxime Dénès
2017-07-12Adding econstr printer to "include" file.Hugo Herbelin
2017-07-12Adding a comment regarding De Bruijn universe indices in the kernel.Pierre-Marie Pédrot
2017-07-11[travis] Display info on tested commit for PR builds.Théo Zimmermann
This is made necessary by the fact that the displayed commit in the header of the build can be outdated if the build was restarted or took a long time to start. Sometimes, it is so old that the link to GitHub is a 404.
2017-07-11Merge PR #871: Update Travis badge following the switch to masterMaxime Dénès
2017-07-11Update Travis badge following the switch to masterThéo Zimmermann
2017-07-11Moving the last bits of abtraction-breaking code out of the kernel.Pierre-Marie Pédrot
2017-07-11Fix nonsensical universe abstraction in the kernel.Pierre-Marie Pédrot
The function turning a side-effect declaration into the corresponding entry was crazily wrong, as it used a named universe context quantifying over DeBruijn universe indices. Declaring such entries resulted in random anomalies. This fixes bug #5641.
2017-07-11Properly handling polymorphic inductive subtyping in the checker.Pierre-Marie Pédrot
This is the followup of the previous commit, this time implementing the correct algorithm in the checker.
2017-07-11Properly handling polymorphic inductive subtyping in the kernel.Pierre-Marie Pédrot
Before this patch, inductive subtyping was enforcing syntactic equality of the variable instance, instead of reasoning up to alpha-renaming.
2017-07-11Cleaning up the implementation of module subtyping in the kernel.Pierre-Marie Pédrot
We export a function in UGraph to check that a polymorphic instance is a subtype of another, instead of rolling up our own in module code. We also add a few tests for module subtyping in presence of polymorphic constants.
2017-07-11Safe API for accessing universe constraints of global references.Pierre-Marie Pédrot
Instead of returning either an instance or the set of constraints, we rather return the corresponding abstracted context. We also push back all uses of abstraction-breaking calls from these functions out of the kernel.
2017-07-11Less footguns in universe handling: remove subst_instance_context.Pierre-Marie Pédrot
This function was lurking around, waiting to bite anybody willing to use it. We use instead a better API, correct and much less error-prone.
2017-07-11Asserting that monomorphic section variables have no abstracted context.Pierre-Marie Pédrot
2017-07-11Getting rid of simple calls to AUContext.instance.Pierre-Marie Pédrot
This function breaks the abstraction barrier of abstract universe contexts, as it provides a way to observe the bound names of such a context. We remove all the uses that can be easily get rid of with the current API.
2017-07-11Merge branch 'v8.7'Maxime Dénès
2017-07-11Merge PR #858: [travis] Remove CompCert version check hack.Maxime Dénès
2017-07-11Merge PR #867: Removing a redundant universe instance information in native ↵Maxime Dénès
compute.
2017-07-11Merge PR #860: use Int.equal instead of polymorphic =Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 01:22:11 +0000