diff options
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 _| |