diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-27 20:04:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-27 20:11:31 +0100 |
| commit | d976efa0b6cfd4be2aa1d9bf8da5a4b266873b15 (patch) | |
| tree | 67536d6ed621a336e6338f4e00af80bb88b2b274 /proofs/tacmach.mli | |
| parent | 37f0149647336f63729b87deb17e3cd7b45c93ca (diff) | |
Removing tactic compatibility layer from Eqdecide.
Diffstat (limited to 'proofs/tacmach.mli')
| -rw-r--r-- | proofs/tacmach.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index d122b0941..897073f36 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 |