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.
---
 kernel/cClosure.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/cClosure.mli')

diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index b6c87b3732..3163833ef3 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -114,7 +114,7 @@ type fterm =
   | FCoFix of cofixpoint * fconstr subs
   | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
   | FLambda of int * (Name.t * constr) list * constr * fconstr subs
-  | FProd of Name.t * fconstr * fconstr
+  | FProd of Name.t * constr * constr * fconstr subs
   | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
   | FEvar of existential * fconstr subs
   | FLIFT of int * fconstr
-- 
cgit v1.2.3