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.
---
 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 3163833ef3..c2d53eed47 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 * constr * constr * fconstr subs
+  | FProd of Name.t * fconstr * 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