aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
authorGaƫtan Gilbert2019-05-20 17:08:38 +0200
committerEnrico Tassi2019-06-04 13:58:42 +0200
commit1ea1e218eed9792685bd7467b63a17fb5ebdbb7e (patch)
tree9bf108186e892513ac4a949a3b6ddf31c05ef328 /stm
parent788b47d9dd70dc9f8057d4a9353ed24f091ea917 (diff)
Rename Proof_global.{t -> stack}
Diffstat (limited to 'stm')
-rw-r--r--stm/stm.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index 64f9e4aacf..0efea0b8e0 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -881,7 +881,7 @@ end = struct (* {{{ *)
let invalidate_cur_state () = cur_id := Stateid.dummy
type proof_part =
- Proof_global.t option *
+ Proof_global.stack option *
int * (* Evarutil.meta_counter_summary_tag *)
int * (* Evd.evar_counter_summary_tag *)
Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)