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 640e294394..c81748a283 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -56,7 +56,7 @@ val hnf_type_of : goal sigma -> constr -> constr val pf_interp_constr : goal sigma -> Coqast.t -> constr val pf_interp_type : goal sigma -> Coqast.t -> constr -val pf_get_hyp : goal sigma -> identifier -> constr option * types +val pf_get_hyp : goal sigma -> identifier -> named_declaration val pf_get_hyp_typ : goal sigma -> identifier -> types val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr |