diff options
| author | Pierre-Marie Pédrot | 2021-01-06 16:20:04 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-18 13:36:46 +0100 |
| commit | 875e410294503b03f0954c94164bd611a5682850 (patch) | |
| tree | b39f48ef592876c10d631850074362245153c8d4 /pretyping/tacred.ml | |
| parent | 5dcf8f4d0fb7419c07b9287db22f6ed6cbf000a4 (diff) | |
Move the two only calls to the strong combinator to their calling site.
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 01819a650b..bd21ecef93 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1040,7 +1040,10 @@ let hnf_constr env sigma c = whd_simpl_orelse_delta_but_fix env sigma (c, []) let whd_simpl env sigma c = applist (whd_simpl_stack env sigma (c, [])) -let simpl env sigma c = strong whd_simpl env sigma c +let simpl env sigma c = + let rec strongrec env t = + map_constr_with_full_binders env sigma push_rel strongrec env (whd_simpl env sigma t) in + strongrec env c (* Reduction at specific subterms *) |