diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e9f84391b6..0257259340 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -989,10 +989,9 @@ let local_whd_state_gen flags sigma = | _ -> s) | Proj (p,c) when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST p) -> - (match (lookup_constant p (Global.env ())).Declarations.const_proj with - | None -> assert false - | Some pb -> whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) - :: stack)) + (let pb = lookup_projection p (Global.env ()) in + whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) + :: stack)) | Case (ci,p,d,lf) -> whrec (d, Stack.Case (ci,p,lf,Cst_stack.empty) :: stack) |