diff options
| author | Pierre-Marie Pédrot | 2019-08-17 19:38:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-25 22:14:34 +0200 |
| commit | df563b34440f6ea14356843b7b1c402a99266910 (patch) | |
| tree | 4d89b0cd0c0dcad257a7528300abf1beed9ae0d4 /kernel | |
| parent | 58a9de2acacb05291d87fe2b656728ae05d59df4 (diff) | |
Clean up InferCumulativity after its move to the kernel.
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 |