From a16be5c566a989e3ba02117ebd912d6025fd54fb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 2 Feb 2018 16:03:37 +0100
Subject: CClosure.unfold_projection: don't catch Not_found, assume env is ok

We can do this after the parent commit (Reductionops.nf_* don't use
empty env)
---
 kernel/cClosure.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index bb5e91d27d..7ed965b4ca 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -851,12 +851,8 @@ 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
+    let pb = lookup_projection p (info_env info) in
+    Some (Zproj (pb.proj_npars, pb.proj_arg, Projection.constant p))
   else None
 
 (*********************************************************************)
-- 
cgit v1.2.3