diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inferCumulativity.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml index 8b5b254f45..3b8c2cd788 100644 --- a/kernel/inferCumulativity.ml +++ b/kernel/inferCumulativity.ml @@ -77,7 +77,7 @@ let infer_sort cv_pb variances s = | CUMUL -> LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances -let infer_table_key _infos variances c = +let infer_table_key variances c = let open Names in match c with | ConstKey (_, u) -> @@ -103,7 +103,7 @@ let rec infer_fterm cv_pb infos variances hd stk = | FRel _ -> infer_stack infos variances stk | FInt _ -> infer_stack infos variances stk | FFlex fl -> - let variances = infer_table_key infos variances fl in + let variances = infer_table_key variances fl in infer_stack infos variances stk | FProj (_,c) -> let variances = infer_fterm CONV infos variances c [] in |