diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 4 | ||||
| -rw-r--r-- | stm/proofBlockDelimiter.mli | 4 | ||||
| -rw-r--r-- | stm/stm.ml | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 0af766219..b8af2bcd5 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -23,8 +23,8 @@ val crawl : static_block_declaration option val unit_val : Stm.DynBlockData.t -val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t -val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet +val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t +val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli index 9784de114..eacd3687a 100644 --- a/stm/proofBlockDelimiter.mli +++ b/stm/proofBlockDelimiter.mli @@ -38,6 +38,6 @@ val crawl : val unit_val : Stm.DynBlockData.t (* Bullets *) -val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t -val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet +val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t +val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t diff --git a/stm/stm.ml b/stm/stm.ml index cbd324f5c..9ea6a305e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2288,7 +2288,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = Proof_global.unfreeze proof; Proof_global.with_current_proof (fun _ p -> feedback ~id:id Feedback.AddedAxiom; - fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ()); + fst (Pfedit.solve Goal_select.SelectAll None tac p), ()); (* STATE SPEC: * - start: Modifies the input state adding a proof. * - end : maybe after recovery command. |