| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-07-17 | Merge PR #862: Adding support for bindings tags to explicit prefix/suffix ↵ | Maxime Dénès | |
| rather than colors | |||
| 2017-07-17 | Merge PR #861: Fix typo in documentation for identity | Maxime Dénès | |
| 2017-07-16 | Fixing what was presumably a typo in the naming conventions file. | Hugo Herbelin | |
| Indeed, "forall x, op x x = x" in not in the list, while this is one of the two standard meanings of idempotence. So, knowing that x, y, ... and not n are used elsewhere for variables names, and elt for constants. Moreover, it is probable that before using consistently x, y and z, I had also used m and n, sometimes. So, a convergent probability that it is (just) a typo. | |||
| 2017-07-16 | Removing a dummy parameter in some FMapPositive statements. | Hugo Herbelin | |
| The statements xelements_bits_lt_1 and xelements_bits_lt_2 had an unexpected extra dependency due to a name collision with a section variable. | |||
| 2017-07-16 | Adapting to 91df40272 (body_of_constant_body moved to global). | Hugo Herbelin | |
| 2017-07-15 | Fixing #5648 (too early decision of tagging ident as keyword in html coqdoc). | Hugo Herbelin | |
| Fix proposed by the reporter, Vincent Laporte. Note that for LaTeX output, the selection of a keyword was already done after checking if the ident is recognized as a Coq ident by coqtop. Incidentally, being now explicit on an wildcard-catching of exceptions. | |||
| 2017-07-14 | Update with non structurally recursive | william-lawvere | |
| 2017-07-14 | Adding debug printers related to universes in the default debugger source file. | Pierre-Marie Pédrot | |
| 2017-07-14 | Fix a typo in dev/changes. | Pierre-Marie Pédrot | |
| 2017-07-14 | Document the changes in API brought by this series of patches. | Pierre-Marie Pédrot | |
| 2017-07-14 | Getting 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-13 | [travis] Update testing to 4.05.0 + Camlp5 7.01 | Emilio Jesus Gallego Arias | |
| 2017-07-13 | Removing 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-13 | Removing 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-13 | Set version to 8.7+alpha. | Maxime Dénès | |
| 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). | |||
| 2017-07-13 | Removing the uses of abstraction-breaking code in Obligations. | Pierre-Marie Pédrot | |
| 2017-07-13 | Remove the function Global.type_of_global_unsafe. | Pierre-Marie Pédrot | |
| 2017-07-13 | The only abstraction-breaking function in Univ is now AUContext.instance. | Pierre-Marie Pédrot | |
| 2017-07-13 | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global. | Pierre-Marie Pédrot | |
| 2017-07-13 | Getting rid of AUContext abstraction breakers in Elimschemes. | Pierre-Marie Pédrot | |
| 2017-07-13 | Getting rid of AUContext abstraction breakers in Discharge. | Pierre-Marie Pédrot | |
| 2017-07-13 | Make 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-13 | Safer 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-13 | Safer API for Global.type_of_global_in_context. | Pierre-Marie Pédrot | |
| We return the abstract context instead of an arbitrary instantiation. | |||
| 2017-07-13 | Getting rid of AUContext abstraction breakers in Record. | Pierre-Marie Pédrot | |
| 2017-07-13 | Getting rid of AUContext abstraction breakers in Search. | Pierre-Marie Pédrot | |
| 2017-07-13 | Getting rid of AUContext abstraction breakers in Recordops. | Pierre-Marie Pédrot | |
| 2017-07-13 | Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel | Maxime Dénès | |
| 2017-07-12 | Adding econstr printer to "include" file. | Hugo Herbelin | |
| 2017-07-12 | format pairs of items for pr_depth to get alternating separators | Paul Steckler | |
| eval thunks once in prlist_sep_lastsep, make code clearer add typeclass debug output test | |||
| 2017-07-12 | Adding a comment regarding De Bruijn universe indices in the kernel. | Pierre-Marie Pédrot | |
| 2017-07-11 | Remove deprecated options from ./configure | Théo Zimmermann | |
| 2017-07-11 | Sync the manual with the deprecation warnings. | Théo Zimmermann | |
| 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-11 | Backtracking on deprecation of Bracketing Last Intro Pattern. | Théo Zimmermann | |
| As per @JasonGross's request who described a use case for this option in https://coq.inria.fr/bugs/show_bug.cgi?id=5633 and pending an alternative solution for this use case. | |||
| 2017-07-11 | Deprecate options that were introduced for compatibility with 8.5. | Théo Zimmermann | |
| 2017-07-11 | Merge PR #871: Update Travis badge following the switch to master | Maxime Dénès | |
| 2017-07-11 | Update Travis badge following the switch to master | Théo Zimmermann | |
| 2017-07-11 | Moving the last bits of abtraction-breaking code out of the kernel. | Pierre-Marie Pédrot | |
| 2017-07-11 | Fix 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-11 | Properly 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-11 | Properly 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-11 | Cleaning 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-11 | Safe 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-11 | Less 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-11 | Asserting that monomorphic section variables have no abstracted context. | Pierre-Marie Pédrot | |
| 2017-07-11 | Getting 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-11 | Merge branch 'v8.7' | Maxime Dénès | |
| 2017-07-11 | Merge PR #858: [travis] Remove CompCert version check hack. | Maxime Dénès | |
| 2017-07-11 | Merge PR #867: Removing a redundant universe instance information in native ↵ | Maxime Dénès | |
| compute. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |