diff options
Diffstat (limited to 'proofs/tacmach.mli')
| -rw-r--r-- | proofs/tacmach.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 581933c83..a808ca419 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -67,12 +67,12 @@ val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> constr val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a -val pf_reduce : +val pf_reduce : (env -> evar_map -> constr -> constr) -> goal sigma -> constr -> constr val pf_whd_betadeltaiota : goal sigma -> constr -> constr -val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list +val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list val pf_hnf_constr : goal sigma -> constr -> constr val pf_red_product : goal sigma -> constr -> constr val pf_nf : goal sigma -> constr -> constr |