diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index fad8623b0..f2a0b6fd1 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -896,6 +896,12 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c = in app_stack (redrec (c, empty_stack)) *) +let whd_simpl_stack = + if Flags.profile then + let key = Profile.declare_profile "whd_simpl_stack" in + Profile.profile3 key whd_simpl_stack + else whd_simpl_stack + (* Same as [whd_simpl] but also reduces constants that do not hide a reducible fix, but does this reduction of constants only until it immediately hides a non reducible fix or a cofix *) |