From 016f2dc3aee608b149097cc08d0720227addc18a Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 29 Apr 2016 11:13:54 +0200
Subject: Fix incorrect cbv reduction of primitive projections. (Bug #4634)

As noticed by Cyprien Mangin, projected terms cannot directly be used as
head values. Indeed, they might be applications (e.g. constructors as in
the bug report) whose arguments would thus be missing from the evaluation
stack when doing any iota-reduction step.

The only case where it would make sense is when the evaluation stack is
empty, as an optimization. Indeed, in that case, the arguments are put on
the stack, and then immediately put back inside the term.
---
 pretyping/cbv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/cbv.ml')

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 43062a0e8d..afd86420e9 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -310,7 +310,7 @@ and cbv_stack_value info env = function
     | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk)))
         when red_set (info_flags info) fIOTA && Projection.unfolded p ->
       let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in
-	cbv_stack_value info env (arg, stk)
+	cbv_stack_value info env (strip_appl arg stk)
 
     (* may be reduced later by application *)
     | (FIXP(fix,env,[||]), APP(appl,TOP)) -> FIXP(fix,env,appl)
-- 
cgit v1.2.3