aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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 a comment regarding De Bruijn universe indices in the kernel.Gravatar Pierre-Marie Pédrot2017-07-12
| |
* | 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.
| * | | Merge PR #863: Fixing environment in warning "Projection value has no head ↵Gravatar Maxime Dénès2017-07-07
| |\ \ \ | | | | | | | | | | | | | | | constant".
| * \ \ \ Merge PR #842: Update the Tutorial.Gravatar Maxime Dénès2017-07-07
| |\ \ \ \
| * \ \ \ \ Merge PR #816: In enter_one, not having exactly one goal is a fatal error of ↵Gravatar Maxime Dénès2017-07-07
| |\ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | the monad.
| * \ \ \ \ \ Merge PR #835: Remove doc/refman/RefMan-ind.texGravatar Maxime Dénès2017-07-07
| |\ \ \ \ \ \
| * | | | | | | Set version to 8.7.0~alpha.Gravatar Maxime Dénès2017-07-07
| | | | | | | |
| * | | | | | | Merge PR #844: Better support for make TIMED=1 on WindowsGravatar Maxime Dénès2017-07-07
| |\ \ \ \ \ \ \
| * \ \ \ \ \ \ \ Merge PR #800: Enable fiat-cryptoGravatar Maxime Dénès2017-07-07
| |\ \ \ \ \ \ \ \
| | | | | | | * | | Fixing environment in warning "Projection value has no head constant".Gravatar Hugo Herbelin2017-07-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Delaying also some computation needed for printing to the time of really printing it.
* | | | | | | | | | Merge PR #853: Clean 'with Definition' implementation.Gravatar Maxime Dénès2017-07-06
|\ \ \ \ \ \ \ \ \ \ | |/ / / / / / / / / |/| | | | | | | | |
| | | | | | | | * | use Int.equal instead of polymorphic =Gravatar Paul Steckler2017-07-05
| | | | | | | | | |
| | | | | | | | | * [travis] Remove CompCert version check hack.Gravatar Emilio Jesus Gallego Arias2017-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 docGravatar Maxime Dénès2017-07-05
|\ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ |/| | | | | | | |
* | | | | | | | | Merge PR #850: Improve grammar in RefMan-Gal and RefMan-synGravatar Maxime Dénès2017-07-05
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #840: Quote $(OCAMLFIND) in CoqMakefile.in for WindowsGravatar Maxime Dénès2017-07-05
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #839: Update .gitignore with doc/tutorial/Tutorial.v.outGravatar Maxime Dénès2017-07-05
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #832: Document an example `Makefile` for `coq_makefile`Gravatar Maxime Dénès2017-07-05
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | * | | | | | Revert fiat-crypto overlayGravatar Jason Gross2017-07-04
| |_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Not a useful overlay. Fiat-crypto has since been updated to pass -compat 8.6.
* | | | | | | | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\ \ \ \ \ \ \ \ \ \ \ \
* | | | | | | | | | | | | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| |_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | |
| | | | | | | * | | | | Removing dead code in Subtyping.Gravatar Pierre-Marie Pédrot2017-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.
| | | | | | | * | | | | Removing a few suspicious functions from the kernel.Gravatar Pierre-Marie Pédrot2017-07-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | These functions were messing with the deferred universe constraints in an error-prone way, and were only used for printing as of today. We inline the one used by the printer instead.
| | | | | | | * | | | | Do not add original constraints to the environment in 'with Definition' check.Gravatar Pierre-Marie Pédrot2017-07-03
| |_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was useless, because immediate constraints are assumed to already be in the current environment, while deferred constraints are useless for the conversion check of the definition types, as they only appear in the opaque body. This also clarifies a bit what is going on in the typing of module constraints w.r.t. global universes.
| | | | | * | | | | | Update RefMan-syn.texGravatar william-lawvere2017-07-01
| | | | | | | | | | |
| | | | | * | | | | | Merge remote-tracking branch 'upstream/trunk' into trunkGravatar William Lawvere2017-07-01
| | | | | |\ \ \ \ \ \ | |_|_|_|_|/ / / / / / |/| | | | | | | | | |
| | | | | * | | | | | RefMan-gal: improve grammarGravatar William Lawvere2017-07-01
| | | | | | | | | | |
| | | | | * | | | | | RefMan-syn: grammar editGravatar William Lawvere2017-07-01
| | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 15:20:53 +0000