diff options
| author | Matthieu Sozeau | 2014-09-06 11:44:53 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-06 11:46:04 +0200 |
| commit | 7a01de25661456406cc2d4a0edcef81af643889c (patch) | |
| tree | 31edb58e9936d488e7a502d2e63ae1e515e6f978 /pretyping | |
| parent | 5d888e0f4943877df04114a0513d70687d9b2c11 (diff) | |
Cleanup code for looking up projection bodies.
Diffstat (limited to 'pretyping')
| -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) |