diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-24 09:56:55 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-29 14:07:34 +0100 |
| commit | a41f8601655f69e71b621dba192342ed0e1f8ec2 (patch) | |
| tree | 921861c20db73501b325befb8ce719f798abc30c /stm/stm.ml | |
| parent | b23df225c7df7883af6ecfa921986cfb6fd3cd7c (diff) | |
[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.
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 2 |
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 |