diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacmach.ml | 1 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index fcba8119d2..fbe201f1a3 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -274,6 +274,7 @@ module New = struct let pf_matches gl pat t = pf_apply ConstrMatching.matches_conv gl pat t let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t + let pf_compute gl t = pf_apply compute gl t let pf_nf_evar gl t = nf_evar (Proofview.Goal.sigma gl) t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index d122b09417..897073f36b 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -152,6 +152,7 @@ module New : sig val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types val pf_whd_betadeltaiota : 'a Proofview.Goal.t -> constr -> constr + val pf_compute : 'a Proofview.Goal.t -> constr -> constr val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map |