diff options
| -rw-r--r-- | pretyping/tacred.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 383d23306..1ba6350b5 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -728,12 +728,14 @@ and whd_simpl_stack env sigma = | Proj (p, c) -> (try - (match recargs (EvalConst p) with - | Some (_, n) when n > 1 -> (* simpl never *) s' - | _ -> - match reduce_projection env sigma p (whd_construct_stack env sigma c) stack with - | Reduced s' -> redrec (applist s') - | NotReducible -> s') + if is_evaluable env (EvalConstRef p) then + (match recargs (EvalConst p) with + | Some (_, n) when n > 1 -> (* simpl never *) s' + | _ -> + match reduce_projection env sigma p (whd_construct_stack env sigma c) stack with + | Reduced s' -> redrec (applist s') + | NotReducible -> s') + else s' with Redelimination -> s') | _ -> |