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


From c4ec9bd2c8a31f5eddea87bbc3f1605ca731d598 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 1 Oct 2018 16:10:37 +0200
Subject: Use a closure for the domain argument of FProd.

The use of a term is not needed for the fast typing algorithm of the
application case, so this tweak brings the best of both worlds.
---
 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 4ce7cdff77..e46d03b743 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -111,7 +111,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
     let variances = infer_fterm CONV infos variances ty [] in
     infer_fterm CONV infos variances bd []
   | FProd (_,dom,codom,e) ->
-    let variances = infer_fterm CONV infos variances (mk_clos e dom) [] in
+    let variances = infer_fterm CONV infos variances dom [] in
     infer_fterm cv_pb infos variances (mk_clos (Esubst.subs_lift e) codom) []
   | FInd (ind, u) ->
     let variances =
-- 
cgit v1.2.3