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 | |
| parent | 5dcf8f4d0fb7419c07b9287db22f6ed6cbf000a4 (diff) | |
Move the two only calls to the strong combinator to their calling site.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 9 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 4 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 5 |
3 files changed, 7 insertions, 11 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index d52be18faa..6185cd3280 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -468,11 +468,6 @@ let safe_meta_value sigma ev = try Some (Evd.meta_value sigma ev) with Not_found -> None -let strong whdfun env sigma t = - let rec strongrec env t = - map_constr_with_full_binders env sigma push_rel strongrec env (whdfun env sigma t) in - strongrec env t - (*************************************) (*** Reduction using bindingss ***) (*************************************) @@ -1269,7 +1264,9 @@ let plain_instance sigma s c = match s with let instance env sigma s c = (* if s = [] then c else *) - strong whd_betaiota env sigma (plain_instance sigma s c) + let rec strongrec env t = + map_constr_with_full_binders env sigma push_rel strongrec env (whd_betaiota env sigma t) in + strongrec env (plain_instance sigma s c) (* pseudo-reduction rule: * [hnf_prod_app env s (Prod(_,B)) N --> B[N] diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 93cb4c190c..140ebdc87d 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -143,10 +143,6 @@ type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type stack_reduction_function = env -> evar_map -> constr -> constr * constr list -(** {6 Reduction Function Operators } *) - -val strong : reduction_function -> reduction_function - (** {6 Generic Optimized Reduction Function using Closures } *) val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function 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 *) |