diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cClosure.ml | 8 |
1 files changed, 2 insertions, 6 deletions
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 (*********************************************************************) |