kernel: cleanup projection unfolding

- use Redflags.red_projection
- share unfold_projection between CClosure and Reduction

1 files changed, 15 insertions, 9 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index b1181157e..bb5e91d27 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -847,6 +847,18 @@ let contract_fix_vect fix =
   in
   (subs_cons(Array.init nfix make_body, env), thisbody)
 
+let unfold_projection info p =
+  if red_projection info.i_flags p
+  then
+    let open Declarations in
+    try
+      let pb = lookup_projection p (info_env info) in
+      Some (Zproj (pb.proj_npars, pb.proj_arg, Projection.constant p))
+    with Not_found ->
+      (* This is possible because sometimes for beta reduction we use a dummy env *)
+      None
+  else None
+
 (*********************************************************************)
 (* A machine that inspects the head of a term until it finds an
    atom or a subterm that may produce a redex (abstraction,
@@ -865,15 +877,9 @@ let rec knh info m stk =
            | (None, stk') -> (m,stk'))
     | FCast(t,_,_) -> knh info t stk
     | FProj (p,c) ->
-      let unf = Projection.unfolded p in
-        if unf || red_set info.i_flags (fCONST (Projection.constant p)) then
-          (match try Some (lookup_projection p (info_env info)) with Not_found -> None with
-	  | None -> (m, stk)
-	  | Some pb ->
-	     knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg,
-				Projection.constant p)
-			 :: zupdate m stk))
-	else (m,stk)
+      (match unfold_projection info p with
+       | None -> (m, stk)
+       | Some s -> knh info c (s :: zupdate m stk))
 
 (* cases where knh stops *)
     | (FFlex _|FLetIn _|FConstruct _|FEvar _|