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 +- vernac/vernacentries.ml | 2 +- vernac/vernacstate.ml | 2 +- vernac/vernacstate.mli | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) (limited to 'vernac') 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 diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7f3410bc1..2f4ec1354 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -484,7 +484,7 @@ let vernac_definition ~atts (local,k) ((loc,id as lid),pl) def = start_proof_and_print (local, atts.polymorphic, DefinitionBody k) [Some (lid,pl), (bl,t)] hook | DefineBody (bl,red_option,c,typ_opt) -> - let red_option = match red_option with + let red_option = match red_option with | None -> None | Some r -> let sigma, env = Pfedit.get_current_context () in diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index eb1359d52..4a1ae14e3 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -8,7 +8,7 @@ type t = { system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) + proof : Proof_global.t; (* proof state *) shallow : bool (* is the state trimmed down (libstack) *) } diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index bcfa49aa3..3ed27ddb7 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -8,7 +8,7 @@ type t = { system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) + proof : Proof_global.t; (* proof state *) shallow : bool (* is the state trimmed down (libstack) *) } -- cgit v1.2.3