From 6c1783de49e0b11f65cc511a94e9ce37f7210562 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 21 Aug 2018 20:05:42 +0200
Subject: Fix #8288: cumulativity inferance ignores args to bound variables

(NB: only variables whose binder is inside the constructor argument,
ie

        Inductive foo := C : forall A : Type -> Type, A Type -> foo.

does not trigger the bug because A becomes a RelKey.)
---
 pretyping/inferCumulativity.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index eb283a0220..be79b8b07d 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -99,7 +99,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
   | FEvar ((_,args),e) ->
     let variances = infer_stack infos variances stk in
     infer_vect infos variances (Array.map (mk_clos e) args)
-  | FRel _ -> variances
+  | FRel _ -> infer_stack infos variances stk
   | FFlex fl ->
     let variances = infer_table_key infos variances fl in
     infer_stack infos variances stk
-- 
cgit v1.2.3