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