aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Merge branch 'v8.7'Gravatar Maxime Dénès2017-07-20
|\
* | Remove the function Global.type_of_global_unsafe.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 Discharge.Gravatar Pierre-Marie Pédrot2017-07-13
* | Make the typeclass implementation fully compatible with universe polymorphism.Gravatar Pierre-Marie Pédrot2017-07-13
* | Safer API for Global.type_of_global_in_context.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
|\ \
| | * Deprecate options that were introduced for compatibility with 8.5.Gravatar Théo Zimmermann2017-07-11
| |/ |/|
| * Safe API for accessing universe constraints of global references.Gravatar Pierre-Marie Pédrot2017-07-11
| * Less footguns in universe handling: remove subst_instance_context.Gravatar Pierre-Marie Pédrot2017-07-11
| * Getting rid of simple calls to AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-11
* | Merge PR #863: Fixing environment in warning "Projection value has no head co...Gravatar Maxime Dénès2017-07-07
|\ \ | |/ |/|
| * Fixing environment in warning "Projection value has no head constant".Gravatar Hugo Herbelin2017-07-07
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\ \
* | | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| |/ |/|
* | Fix a bug in cumulativityGravatar Amin Timany2017-06-16
* | Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* | Fix a bugGravatar Amin Timany2017-06-16
* | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
* | Fix bugsGravatar Amin Timany2017-06-16
* | Squashed commit of the following:Gravatar Amin Timany2017-06-16
* | Make unification use subtyping info of inductivesGravatar Amin Timany2017-06-16
* | Use inductive subtyping for conv/cumulGravatar Amin Timany2017-06-16
* | Subtyping inference for inductoves and recordsGravatar Amin Timany2017-06-16
* | Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
| * Merge PR#713: Bump year in headers.Gravatar Maxime Dénès2017-06-15
| |\
| * \ Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Maxime Dénès2017-06-15
| |\ \
* | \ \ Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\ \ \ \
* \ \ \ \ Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\ \ \ \ \
| | * | | | Deprecate options that were introduced for compatibility with 8.2.Gravatar Guillaume Melquiond2017-06-14
| | * | | | Remove options deprecated since 8.4.Gravatar Guillaume Melquiond2017-06-14
| | * | | | Remove support for Coq 8.3.Gravatar Guillaume Melquiond2017-06-14
| | * | | | Remove support for Coq 8.2.Gravatar Guillaume Melquiond2017-06-14
| |/ / / / |/| | | |
* | | | | Merge PR#714: Print feature Proof-of-Concept (episode 2)Gravatar Maxime Dénès2017-06-13
|\ \ \ \ \
| | * | | | A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
| |/ / / / |/| | | |
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \ \ \ \ | | |/ / / | |/| | |
* | | | | Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* | | | | Merge PR#716: Don't double up on periods in anomaliesGravatar Maxime Dénès2017-06-06
|\ \ \ \ \
* \ \ \ \ \ Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...Gravatar Maxime Dénès2017-06-05
|\ \ \ \ \ \
| | | | | * | Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Matthieu Sozeau2017-06-05
| | | | * | | Added support for a side effect on constants in reduction functions.Gravatar Thomas Sibut-Pinote2017-06-04
| |_|_|/ / / |/| | | | |
| | * | | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | * | | | Don't double up on periods in anomaliesGravatar Jason Gross2017-06-02
| |/ / / / |/| | | |
* | | | | Merge PR#670: Postponing of universe constraints unification in term equality.Gravatar Maxime Dénès2017-06-01
|\ \ \ \ \
* \ \ \ \ \ Merge PR#696: Trunk+cleanup constr of globalGravatar Maxime Dénès2017-06-01
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#561: Improving the Name APIGravatar Maxime Dénès2017-06-01
|\ \ \ \ \ \ \
| | | | | | | * Bump year in headers.Gravatar Maxime Dénès2017-06-01
* | | | | | | | Merge PR#694: Fixing #5523 (missing support for complex constructions in recu...Gravatar Maxime Dénès2017-06-01
|\ \ \ \ \ \ \ \
| | | | | | * \ \ Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake (...Gravatar Maxime Dénès2017-05-31
| | | | | | |\ \ \ | | | | | | | |_|/ | | | | | | |/| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-28 18:52:55 +0000