aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-16 15:44:44 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-03-09 16:29:06 +0100
commit17a0dccfe91d6f837ce285e62b8d843720f8c1a1 (patch)
tree605a2dae6692cec6503ab5fcdce7c90421db26f0 /vernac
parent3d86afb36517c9ba4200289e169239f7fa54fca1 (diff)
Allow using cumulativity without forcing strict constraints.
Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative inductive would try to generate a constraint [i = j] and use cumulativity only if this resulted in an inconsistency. This is confusingly different from the behaviour with [Type] and means cumulativity can only be used to lift between universes related by strict inequalities. (This isn't a kernel restriction so there might be some workaround to send the kernel the right constraints, but not in a nice way.) See modified test for more details of what is now possible. Technical notes: When universe constraints were inferred by comparing the shape of terms without reduction, cumulativity was not used and so too-strict equality constraints were generated. Then in order to use cumulativity we had to make this comparison fail to fall back to full conversion. When unifiying 2 instances of a cumulative inductive type, if there are any Irrelevant universes we try to unify them if they are flexible.
Diffstat (limited to 'vernac')
-rw-r--r--vernac/obligations.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 4f16e1cf6..064e40b9b 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -1,5 +1,4 @@
open Printf
-open Globnames
open Libobject
open Entries
open Decl_kinds