diff options
| -rw-r--r-- | pretyping/reductionops.ml | 9 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 4 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 5 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
4 files changed, 7 insertions, 15 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 *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b40bdbc25e..aef6596e8f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1244,8 +1244,6 @@ let force_destruction_arg with_evars env sigma c = (* tactic "cut" (actually modus ponens) *) (****************************************) -let normalize_cut = false - let cut c = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1260,8 +1258,6 @@ let cut c = | sigma, s -> let r = Sorts.relevance_of_sort s in let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in - (* Backward compat: normalize [c]. *) - let c = if normalize_cut then strong whd_betaiota env sigma c else c in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine ~typecheck:false begin fun h -> let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in |