From a41f8601655f69e71b621dba192342ed0e1f8ec2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 24 Nov 2017 09:56:55 +0100 Subject: [proof] [api] Rename proof types in preparation for functionalization. In particular `Proof_global.t` will become a first class object for the upper parts of the system in a next commit. --- vernac/lemmas.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/lemmas.mli') diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 1b1304db5..a4854b4a6 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -56,7 +56,7 @@ val standard_proof_terminator : (** {6 ... } *) (** A hook the next three functions pass to cook_proof *) -val set_save_hook : (Proof.proof -> unit) -> unit +val set_save_hook : (Proof.t -> unit) -> unit val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit -- cgit v1.2.3