aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layersGravatar Maxime Dénès2017-07-17
|\
* \ Merge PR #881: Adapting base_include to 91df40272 (body_of_constant_body ↵Gravatar Maxime Dénès2017-07-17
|\ \ | | | | | | | | | moved to Global).
* \ \ Merge PR #879: Adding debug printers related to universesGravatar Maxime Dénès2017-07-17
|\ \ \
* \ \ \ Merge PR #874: Adding econstr printer to "include" file.Gravatar Maxime Dénès2017-07-17
|\ \ \ \
* \ \ \ \ Merge PR #872: [travis] Display info on tested commit for PR builds.Gravatar Maxime Dénès2017-07-17
|\ \ \ \ \
* \ \ \ \ \ Merge PR #865: RefMan-ext: fix some typosGravatar Maxime Dénès2017-07-17
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #862: Adding support for bindings tags to explicit prefix/suffix ↵Gravatar Maxime Dénès2017-07-17
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | rather than colors
| | | | | | * | Adapting to 91df40272 (body_of_constant_body moved to global).Gravatar Hugo Herbelin2017-07-16
| |_|_|_|_|/ / |/| | | | | |
| | * | | | | Update with non structurally recursiveGravatar william-lawvere2017-07-14
| | | | | | |
| | | | | * | Adding debug printers related to universes in the default debugger source file.Gravatar Pierre-Marie Pédrot2017-07-14
| |_|_|_|/ / |/| | | | |
| | | | | * Fix a typo in dev/changes.Gravatar Pierre-Marie Pédrot2017-07-14
| | | | | |
| | | | | * Document the changes in API brought by this series of patches.Gravatar Pierre-Marie Pédrot2017-07-14
| | | | | |
| | | | | * Getting rid of abstraction breaking code in tclABSTRACT.Gravatar Pierre-Marie Pédrot2017-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.
| | | | | * Removing a use of AUContext.instance in the STM.Gravatar Pierre-Marie Pédrot2017-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.Gravatar Pierre-Marie Pédrot2017-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.
| | | | | * Removing the uses of abstraction-breaking code in Obligations.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | |
| | | | | * Remove the function Global.type_of_global_unsafe.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | |
| | | | | * The only abstraction-breaking function in Univ is now AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | |
| | | | | * Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | |
| | | | | * Getting rid of AUContext abstraction breakers in Elimschemes.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | |
| | | | | * Getting rid of AUContext abstraction breakers in Discharge.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | |
| | | | | * Make the typeclass implementation fully compatible with universe polymorphism.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This essentially means storing the abstract universe context in the typeclass data, and abstracting it when necessary.
| | | | | * Safer API for Global.body_of_constant and variants.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We aditionally return the abstract universe context inside the option. This is relatively painless as most uses were using the option as a boolean.
| | | | | * Safer API for Global.type_of_global_in_context.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | | | | | | | | | | | | | | | | | | | | We return the abstract context instead of an arbitrary instantiation.
| | | | | * Getting rid of AUContext abstraction breakers in Record.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | |
| | | | | * Getting rid of AUContext abstraction breakers in Search.Gravatar Pierre-Marie Pédrot2017-07-13
| | | | | |
| | | | | * Getting rid of AUContext abstraction breakers in Recordops.Gravatar Pierre-Marie Pédrot2017-07-13
| |_|_|_|/ |/| | | |
* | | | | Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: KernelGravatar Maxime Dénès2017-07-13
|\ \ \ \ \
| | | | | * Adding econstr printer to "include" file.Gravatar Hugo Herbelin2017-07-12
| |_|_|_|/ |/| | | |
| * | | | Adding a comment regarding De Bruijn universe indices in the kernel.Gravatar Pierre-Marie Pédrot2017-07-12
| | | | |
| | | | * [travis] Display info on tested commit for PR builds.Gravatar Théo Zimmermann2017-07-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | Merge PR #871: Update Travis badge following the switch to masterGravatar Maxime Dénès2017-07-11
|\ \ \ \ \
| * | | | | Update Travis badge following the switch to masterGravatar Théo Zimmermann2017-07-11
| | |_|_|/ | |/| | |
| | * | | Moving the last bits of abtraction-breaking code out of the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | |
| | * | | Fix nonsensical universe abstraction in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | Properly handling polymorphic inductive subtyping in the checker.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | | | | | | | | | | | | | | | | | | This is the followup of the previous commit, this time implementing the correct algorithm in the checker.
| | * | | Properly handling polymorphic inductive subtyping in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | | | | | | | | | | | | | | | | | | Before this patch, inductive subtyping was enforcing syntactic equality of the variable instance, instead of reasoning up to alpha-renaming.
| | * | | Cleaning up the implementation of module subtyping in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | Safe API for accessing universe constraints of global references.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | Less footguns in universe handling: remove subst_instance_context.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | Asserting that monomorphic section variables have no abstracted context.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | |
| | * | | Getting rid of simple calls to AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-11
| |/ / / | | | | | | | | | | | | | | | | | | | | 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.
* | | | Merge branch 'v8.7'Gravatar Maxime Dénès2017-07-11
|\ \ \ \ | |/ / / |/| | |
| * | | Merge PR #858: [travis] Remove CompCert version check hack.Gravatar Maxime Dénès2017-07-11
| |\ \ \
* | \ \ \ Merge PR #867: Removing a redundant universe instance information in native ↵Gravatar Maxime Dénès2017-07-11
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | compute.
| | * \ \ \ Merge PR #860: use Int.equal instead of polymorphic =Gravatar Maxime Dénès2017-07-11
| | |\ \ \ \
| * | | | | | Removing a redundant universe instance information in native compute.Gravatar Pierre-Marie Pédrot2017-07-10
|/ / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Global declarations used to carry universe instances with them, but it turns out this information is not used anywhere. Instead, instances were already properly encoded as the first argument of polymorphic definitions.
| | | | * | Adding support for bindings tags to explicit prefix/suffix rather than colors.Gravatar Hugo Herbelin2017-07-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is usable for no-color terminal. For instance, a typical application in mind is the Coq-generate names marker which can be rendered with a color if the interface supports it and a prefix "~" if the interface does not support colors.
| | | | | * RefMan-ext: fix some typosGravatar William Lawvere2017-07-07
| |_|_|_|/ |/| | | |
| * | | | Merge PR #863: Fixing environment in warning "Projection value has no head ↵Gravatar Maxime Dénès2017-07-07
| |\ \ \ \ | | | | | | | | | | | | | | | | | | constant".
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-25 01:38:11 +0000