From 82f7c721ea066a4776be09bd40444cf491f3659e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 May 2018 12:12:43 +0200
Subject: Do not wrap FProd return types in a closure.

There is little point to this as the type is dependent on an open value and
is never computed further.
---
 pretyping/inferCumulativity.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index 9762d0f1d9..4ce7cdff77 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -110,9 +110,9 @@ let rec infer_fterm cv_pb infos variances hd stk =
     let (_,ty,bd) = destFLambda mk_clos hd in
     let variances = infer_fterm CONV infos variances ty [] in
     infer_fterm CONV infos variances bd []
-  | FProd (_,dom,codom) ->
-    let variances = infer_fterm CONV infos variances dom [] in
-    infer_fterm cv_pb infos variances codom []
+  | FProd (_,dom,codom,e) ->
+    let variances = infer_fterm CONV infos variances (mk_clos e dom) [] in
+    infer_fterm cv_pb infos variances (mk_clos (Esubst.subs_lift e) codom) []
   | FInd (ind, u) ->
     let variances =
       if Instance.is_empty u then variances
-- 
cgit v1.2.3