diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-06 11:44:53 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-06 11:46:04 +0200 |
| commit | 7a01de25661456406cc2d4a0edcef81af643889c (patch) | |
| tree | 31edb58e9936d488e7a502d2e63ae1e515e6f978 /checker/closure.ml | |
| parent | 5d888e0f4943877df04114a0513d70687d9b2c11 (diff) | |
Cleanup code for looking up projection bodies.
Diffstat (limited to 'checker/closure.ml')
| -rw-r--r-- | checker/closure.ml | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/checker/closure.ml b/checker/closure.ml index 6f19fc59f..879146284 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -799,13 +799,11 @@ let rec knh info m stk = | FCast(t,_,_) -> knh info t stk | FProj (p,c) -> - (* if red_set info.i_flags (fCONST p) then *) - (match try Some (lookup_projection p (info.i_env)) with Not_found -> None with - | None -> (m, stk) - | Some pb -> - knh info c (Zproj (pb.proj_npars, pb.proj_arg, p) - :: zupdate m stk)) - (* else (m,stk) *) + if red_set info.i_flags (fCONST p) then + (let pb = lookup_projection p (info.i_env) in + knh info c (Zproj (pb.proj_npars, pb.proj_arg, p) + :: zupdate m stk)) + else (m,stk) (* cases where knh stops *) | (FFlex _|FLetIn _|FConstruct _|FEvar _| |