diff options
Diffstat (limited to 'proofs/tacmach.mli')
| -rw-r--r-- | proofs/tacmach.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 931f988dd4..7031852f57 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -66,7 +66,7 @@ val pf_get_new_ids : identifier list -> goal sigma -> identifier list val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr - +val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a val pf_reduce : (env -> evar_map -> constr -> constr) -> goal sigma -> constr -> constr |