diff options
| author | Matthieu Sozeau | 2014-02-14 14:19:53 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:57 +0200 |
| commit | df5e18302e113370906d9ca0b2a2e96dcaccbf0a (patch) | |
| tree | f2610a6048d872247575abd7c9dfe2c9e0873254 | |
| parent | 98e9c806dee5ab8c3430000a9a9fd5d478662ae6 (diff) | |
Honor the Opaque flag for projections in simpl.
| -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 383d233069..1ba6350b5c 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') | _ -> |