aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/vernacstate.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/vernacstate.mli')
-rw-r--r--vernac/vernacstate.mli2
1 files changed, 1 insertions, 1 deletions
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) *)
}