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 770d0940a..de96f8510 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -95,7 +95,7 @@ val pr_glls : goal list sigma -> Pp.t (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a - val pf_global : Id.t -> Proofview.Goal.t -> Globnames.global_reference + val pf_global : Id.t -> Proofview.Goal.t -> GlobRef.t (** FIXME: encapsulate the level in an existential type. *) val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a |