diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-02 16:03:37 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-02 16:03:37 +0100 |
| commit | a16be5c566a989e3ba02117ebd912d6025fd54fb (patch) | |
| tree | 719add667553f3fddb9e86860ee6bc104e34278a /kernel | |
| parent | e6353e9ef6542b444391a46d9557ebf3a6443947 (diff) | |
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)
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 bb5e91d27..7ed965b4c 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 (*********************************************************************) |