diff options
Diffstat (limited to 'pretyping/tacred.mli')
| -rw-r--r-- | pretyping/tacred.mli | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 84cc87e7f0..0ff5154f60 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -35,11 +35,15 @@ val red_product : reduction_function (* Red (raise Redelimination if nothing reducible) *) val try_red_product : reduction_function -(* Hnf *) -val hnf_constr : reduction_function - (* Simpl *) -val nf : reduction_function +val simpl : reduction_function + +(* Simpl only at the head *) +val whd_simpl : reduction_function + +(* Hnf: like whd_simpl but force delta-reduction of constants that do + not immediately hide a non reducible fix or cofix *) +val hnf_constr : reduction_function (* Unfold *) val unfoldn : @@ -79,3 +83,8 @@ val reduce_to_atomic_ref : val contextually : bool -> int list * constr -> reduction_function -> reduction_function + +(* Compatibility *) +(* use [simpl] instead of [nf] *) +val nf : reduction_function + |