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 /proofs/proof_bullet.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 'proofs/proof_bullet.ml')
| -rw-r--r-- | proofs/proof_bullet.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 4f575ab4b..214916331 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -25,8 +25,8 @@ let pr_bullet b = type behavior = { name : string; - put : proof -> t -> proof; - suggest: proof -> Pp.t + put : Proof.t -> t -> Proof.t; + suggest: Proof.t -> Pp.t } let behaviors = Hashtbl.create 4 @@ -110,7 +110,7 @@ module Strict = struct let push (b:t) pr = focus bullet_cond (b::get_bullets pr) 1 pr - let suggest_bullet (prf : proof): suggestion = + let suggest_bullet (prf : Proof.t): suggestion = if is_done prf then ProofFinished else if not (no_focused_goal prf) then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *) @@ -137,7 +137,7 @@ module Strict = struct in loop prf - let rec pop_until (prf : proof) bul : proof = + let rec pop_until (prf : Proof.t) bul : Proof.t = let prf', b = pop prf in if bullet_eq bul b then prf' else pop_until prf' bul |