diff options
| author | Pierre-Marie Pédrot | 2016-11-24 12:07:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:36 +0100 |
| commit | fa638c3e71752b6a59261776b36f1bed7d9c26d2 (patch) | |
| tree | 4e0b7b249a585edf0584e650a0c79ea441e9c9cc /pretyping | |
| parent | a327ae04966aa1c7786ae32157516e934068ea89 (diff) | |
Cc API using EConstr.
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 |