From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 pretyping/cbv.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'pretyping/cbv.ml')

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 43062a0e..84bf849e 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -10,7 +10,7 @@ open Util
 open Names
 open Term
 open Vars
-open Closure
+open CClosure
 open Esubst
 
 (**** Call by value reduction ****)
@@ -156,7 +156,7 @@ let strip_appl head stack =
 
 (* Tests if fixpoint reduction is possible. *)
 let fixp_reducible flgs ((reci,i),_) stk =
-  if red_set flgs fIOTA then
+  if red_set flgs fFIX then
     match stk with
       | APP(appl,_) ->
           Array.length appl > reci.(i) &&
@@ -168,7 +168,7 @@ let fixp_reducible flgs ((reci,i),_) stk =
     false
 
 let cofixp_reducible flgs _ stk =
-  if red_set flgs fIOTA then
+  if red_set flgs fCOFIX then
     match stk with
       | (CASE _ | APP(_,CASE _)) -> true
       | _ -> false
@@ -296,21 +296,21 @@ and cbv_stack_value info env = function
 
     (* constructor in a Case -> IOTA *)
     | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,ci,env,stk)))
-            when red_set (info_flags info) fIOTA ->
+            when red_set (info_flags info) fMATCH ->
 	let cargs =
           Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in
         cbv_stack_term info (stack_app cargs stk) env br.(n-1)
 
     (* constructor of arity 0 in a Case -> IOTA *)
     | (CONSTR(((_,n),u),[||]), CASE(_,br,_,env,stk))
-            when red_set (info_flags info) fIOTA ->
+            when red_set (info_flags info) fMATCH ->
                     cbv_stack_term info stk env br.(n-1)
 
     (* constructor in a Projection -> IOTA *)
     | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk)))
-        when red_set (info_flags info) fIOTA && Projection.unfolded p ->
+        when red_set (info_flags info) fMATCH && 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