diff options
| author | Gaëtan Gilbert | 2019-05-20 17:08:38 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 13:58:42 +0200 |
| commit | 1ea1e218eed9792685bd7467b63a17fb5ebdbb7e (patch) | |
| tree | 9bf108186e892513ac4a949a3b6ddf31c05ef328 /proofs/proof_global.ml | |
| parent | 788b47d9dd70dc9f8057d4a9353ed24f091ea917 (diff) | |
Rename Proof_global.{t -> stack}
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 8d7960829b..e26577e8bd 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -56,7 +56,7 @@ type pstate = { (* The head of [t] is the actual current proof, the other ones are to be resumed when the current proof is closed or aborted. *) -type t = pstate * pstate list +type stack = pstate * pstate list let pstate_map f (pf, pfl) = (f pf, List.map f pfl) @@ -77,7 +77,7 @@ let maybe_push ~ontop = function (*** Proof Global manipulation ***) -let get_all_proof_names (pf : t) = +let get_all_proof_names (pf : stack) = let (pn, pns) = pstate_map Proof.(function pf -> (data pf.proof).name) pf in pn :: pns |