diff options
| author | Pierre-Marie Pédrot | 2020-04-01 17:39:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-10 15:04:06 +0200 |
| commit | cf60564b9e6cdfa35fe8c256f6785e23a2afde61 (patch) | |
| tree | c647d30d9d8ed572ff43717c09f0d0c55356cb9a /pretyping | |
| parent | 2a79abc613bdf19b53685a40c993f964455904fe (diff) | |
Further cleanup: remove the local_reduction_function type.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 11 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 3 | ||||
| -rw-r--r-- | pretyping/unification.ml | 3 |
3 files changed, 2 insertions, 15 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 4d083664f7..15bf9667b3 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -604,7 +604,6 @@ end type state = constr * constr Stack.t type reduction_function = env -> evar_map -> constr -> constr -type local_reduction_function = evar_map -> constr -> constr type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type contextual_stack_reduction_function = @@ -649,16 +648,6 @@ let strong whdfun env sigma t = map_constr_with_full_binders sigma push_rel strongrec env (whdfun env sigma t) in strongrec env t -let local_strong whdfun sigma = - let rec strongrec t = EConstr.map sigma strongrec (whdfun sigma t) in - strongrec - -let rec strong_prodspine redfun sigma c = - let x = redfun sigma c in - match EConstr.kind sigma x with - | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b) - | _ -> x - (*************************************) (*** Reduction using bindingss ***) (*************************************) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 555c4be971..be91f688e7 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -128,7 +128,6 @@ end type state = constr * constr Stack.t type reduction_function = env -> evar_map -> constr -> constr -type local_reduction_function = evar_map -> constr -> constr type e_reduction_function = env -> evar_map -> constr -> evar_map * constr @@ -150,8 +149,6 @@ val strong_with_flags : (CClosure.RedFlags.reds -> reduction_function) -> (CClosure.RedFlags.reds -> reduction_function) val strong : reduction_function -> reduction_function -val local_strong : local_reduction_function -> local_reduction_function -val strong_prodspine : local_reduction_function -> local_reduction_function (*i val stack_reduction_of_reduction : 'a reduction_function -> 'a state_reduction_function diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ab99bdc777..88eec5ea01 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1641,7 +1641,8 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = (fun test -> match test.testing_state with | None -> None | Some (sigma,_,l) -> - let c = applist (local_strong whd_meta sigma c, l) in + let rec strong_whd_meta t = EConstr.map sigma strong_whd_meta (whd_meta sigma t) in + let c = applist (strong_whd_meta c, l) in Some (sigma, c)) let make_eq_test env evd c = |