From df563b34440f6ea14356843b7b1c402a99266910 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 17 Aug 2019 19:38:47 +0200
Subject: Clean up InferCumulativity after its move to the kernel.

---
 kernel/inferCumulativity.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3