diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 8 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 1 |
2 files changed, 9 insertions, 0 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 45e7abcb79..c796a91caa 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1221,6 +1221,14 @@ let clos_norm_flags flgs env sigma t = (CClosure.inject (EConstr.Unsafe.to_constr t))) with e when is_anomaly e -> error "Tried to normalize ill-typed term" +let clos_whd_flags flgs env sigma t = + try + let evars ev = safe_evar_value sigma ev in + EConstr.of_constr (CClosure.whd_val + (CClosure.create_clos_infos ~evars flgs env) + (CClosure.inject (EConstr.Unsafe.to_constr t))) + with e when is_anomaly e -> error "Tried to normalize ill-typed term" + let nf_beta = clos_norm_flags CClosure.beta (Global.env ()) let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ()) let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta (Global.env ()) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index add1d186bb..8aaeeb2c21 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -149,6 +149,7 @@ val iterate_whd_gen : bool -> CClosure.RedFlags.reds -> (** {6 Generic Optimized Reduction Function using Closures } *) val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function +val clos_whd_flags : CClosure.RedFlags.reds -> reduction_function (** Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) val nf_beta : local_reduction_function |