aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/uGraph.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/uGraph.ml')
-rw-r--r--kernel/uGraph.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index f1e8d1031..5dca69c16 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -833,7 +833,7 @@ let sort_universes g =
(** Subtyping of polymorphic contexts *)
let check_subtype univs ctxT ctx =
- if AUContext.size ctx == AUContext.size ctx then
+ if AUContext.size ctxT == AUContext.size ctx then
let (inst, cst) = UContext.dest (AUContext.repr ctx) in
let cstT = UContext.constraints (AUContext.repr ctxT) in
let push accu v = add_universe v false accu in