From 507cd85244db835f13bc65cb9b92aa903180989c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 16 Feb 2018 16:07:17 +0100
Subject: Fix reduction flags in inferCumulativity

The only difference is when we have a rel local definition in the
initial environment, which isn't actually possible. However that
depends on the specific way we treat parameters.
---
 pretyping/inferCumulativity.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index a0a8276c5c..b369fe4e45 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -159,8 +159,7 @@ and infer_vect infos variances v =
 
 let infer_term cv_pb env variances c =
   let open CClosure in
-  let reds = RedFlags.red_add_transparent betaiotazeta Names.full_transparent_state in
-  let infos = create_clos_infos reds env in
+  let infos = create_clos_infos all env in
   infer_fterm cv_pb infos variances (CClosure.inject c) []
 
 let infer_arity_constructor env variances arcn is_arity params =
-- 
cgit v1.2.3