diff options
Diffstat (limited to 'proofs/tacmach.ml')
| -rw-r--r-- | proofs/tacmach.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index fa0d0362..4238d1e3 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -84,6 +84,7 @@ let pf_nf = pf_reduce simpl let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota) let pf_compute = pf_reduce compute let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) +let pf_unsafe_type_of = pf_reduce unsafe_type_of let pf_type_of = pf_reduce type_of let pf_get_type_of = pf_reduce Retyping.get_type_of @@ -172,6 +173,9 @@ module New = struct let pf_env = Proofview.Goal.env let pf_concl = Proofview.Goal.concl + let pf_unsafe_type_of gl t = + pf_apply unsafe_type_of gl t + let pf_type_of gl t = pf_apply type_of gl t |