aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/stm.ml')
-rw-r--r--stm/stm.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index ab44cc98b..8aa832da8 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -762,7 +762,7 @@ end = struct (* {{{ *)
let fix_exn_ref = ref (fun x -> x)
type proof_part =
- Proof_global.state * Summary.frozen_bits (* only meta counters *)
+ Proof_global.t * Summary.frozen_bits (* only meta counters *)
type partial_state =
[ `Full of Vernacstate.t