aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-01 09:25:56 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-01 09:25:56 +0100
commit895900eb4c3f030e9490d211a4969de933ec2f9b (patch)
treec4d454c201276b0953fe3383c46f76423c8ab515 /vernac
parente29993c250164b9486d4d7ffdebb9bfee4a2828f (diff)
parenta41f8601655f69e71b621dba192342ed0e1f8ec2 (diff)
Merge PR #6233: [proof] [api] Rename proof types in preparation for functionalization.
Diffstat (limited to 'vernac')
-rw-r--r--vernac/lemmas.mli2
-rw-r--r--vernac/vernacentries.ml2
-rw-r--r--vernac/vernacstate.ml2
-rw-r--r--vernac/vernacstate.mli2
4 files changed, 4 insertions, 4 deletions
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 63f358a9d..f8ec05fdb 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -484,7 +484,7 @@ let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def =
start_proof_and_print (local, atts.polymorphic, DefinitionBody kind)
[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) *)
}