Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 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 | 2017-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. | Pierre-Marie Pédrot | 2017-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. | Pierre-Marie Pédrot | 2017-07-13 |
| | | | | We return the abstract context instead of an arbitrary instantiation. | ||
* | 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-13 |
|\ | |||
| * | Adding a comment regarding De Bruijn universe indices in the kernel. | Pierre-Marie Pédrot | 2017-07-12 |
| | | |||
* | | 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 | 2017-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. | Pierre-Marie Pédrot | 2017-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. | Pierre-Marie Pédrot | 2017-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. | Pierre-Marie Pédrot | 2017-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. | Pierre-Marie Pédrot | 2017-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. | Pierre-Marie Pédrot | 2017-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. | Pierre-Marie Pédrot | 2017-07-11 |
| | | | |||
| | * | Getting rid of simple calls to AUContext.instance. | Pierre-Marie Pédrot | 2017-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' | 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 | 2017-07-11 |
|\ \ \ | | | | | | | | | | | | | compute. | ||
| | * \ | Merge PR #860: use Int.equal instead of polymorphic = | Maxime Dénès | 2017-07-11 |
| | |\ \ | |||
| * | | | | Removing a redundant universe instance information in native compute. | Pierre-Marie Pédrot | 2017-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. | ||
| * | | | Merge PR #863: Fixing environment in warning "Projection value has no head ↵ | Maxime Dénès | 2017-07-07 |
| |\ \ \ | | | | | | | | | | | | | | | | constant". | ||
| * \ \ \ | Merge PR #842: Update the Tutorial. | Maxime Dénès | 2017-07-07 |
| |\ \ \ \ | |||
| * \ \ \ \ | Merge PR #816: In enter_one, not having exactly one goal is a fatal error of ↵ | Maxime Dénès | 2017-07-07 |
| |\ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | the monad. | ||
| * \ \ \ \ \ | Merge PR #835: Remove doc/refman/RefMan-ind.tex | Maxime Dénès | 2017-07-07 |
| |\ \ \ \ \ \ | |||
| * | | | | | | | Set version to 8.7.0~alpha. | Maxime Dénès | 2017-07-07 |
| | | | | | | | | |||
| * | | | | | | | Merge PR #844: Better support for make TIMED=1 on Windows | Maxime Dénès | 2017-07-07 |
| |\ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR #800: Enable fiat-crypto | Maxime Dénès | 2017-07-07 |
| |\ \ \ \ \ \ \ \ | |||
| | | | | | | * | | | Fixing environment in warning "Projection value has no head constant". | Hugo Herbelin | 2017-07-07 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Delaying also some computation needed for printing to the time of really printing it. | ||
* | | | | | | | | | | Merge PR #853: Clean 'with Definition' implementation. | Maxime Dénès | 2017-07-06 |
|\ \ \ \ \ \ \ \ \ \ | |/ / / / / / / / / |/| | | | | | | | | | |||
| | | | | | | | * | | use Int.equal instead of polymorphic = | Paul Steckler | 2017-07-05 |
| | | | | | | | | | | |||
| | | | | | | | | * | [travis] Remove CompCert version check hack. | Emilio Jesus Gallego Arias | 2017-07-05 |
| | | | | | | | |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We now pass `-ignore-coq-version` to CompCert's configure (cf AbsInt/CompCert#188) , thanks to @xavierleroy . | ||
* | | | | | | | | | Merge PR #837: Add inversion_sigma to CHANGES and to doc | Maxime Dénès | 2017-07-05 |
|\ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ |/| | | | | | | | | |||
* | | | | | | | | | Merge PR #850: Improve grammar in RefMan-Gal and RefMan-syn | Maxime Dénès | 2017-07-05 |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #840: Quote $(OCAMLFIND) in CoqMakefile.in for Windows | Maxime Dénès | 2017-07-05 |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #839: Update .gitignore with doc/tutorial/Tutorial.v.out | Maxime Dénès | 2017-07-05 |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #832: Document an example `Makefile` for `coq_makefile` | Maxime Dénès | 2017-07-05 |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | * | | | | | | Revert fiat-crypto overlay | Jason Gross | 2017-07-04 |
| |_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Not a useful overlay. Fiat-crypto has since been updated to pass -compat 8.6. | ||
* | | | | | | | | | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-07-04 |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* | | | | | | | | | | | | | Bump year in headers. | Pierre-Marie Pédrot | 2017-07-04 |
| |_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | |||
| | | | | | | * | | | | | Removing dead code in Subtyping. | Pierre-Marie Pédrot | 2017-07-04 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This code was a sketch of what to do when we properly implement module-level handling of instanciation of definitions by inductive types. It was completely dead code, called after an error, and somewhat incorrect. Instead of letting it bitrot, we remove it. |