diff options
| author |  Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-03 11:24:42 +0100 |
|---|---|---|
| committer | Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 22:51:35 +0100 |
| commit | 11a26905d2406b99a2a9b040891996f95df1d2ce (patch) | |
| tree | f69da2566db52f425c2a0f66caec226bed7a34ef /ide/wg_ProofView.ml | |
| parent | f1d63425ca674f8cd9cb25eeec9f35825190162f (diff) | |
ide/wg_ProofView: Do not refer to the {Proof} internal module, use {Interface} instead.
Diffstat (limited to 'ide/wg_ProofView.ml')
| -rw-r--r-- | ide/wg_ProofView.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 62ebaf4d9..74e63a090 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -93,7 +93,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with in proof#buffer#insert (goal_str 1 goals_cnt); proof#buffer#insert ~tags cur_goal; - proof#buffer#insert "\n" + proof#buffer#insert "\n" in (* Insert remaining goals (no hypotheses) *) let fold_goal i _ { Interface.goal_ccl = g } = @@ -104,7 +104,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with ignore(proof#buffer#place_cursor ~where:(proof#buffer#end_iter#backward_to_tag_toggle - (Some Tags.Proof.goal))); + (Some Tags.Proof.goal))); ignore(proof#scroll_to_mark ~use_align:true ~yalign:0.95 `INSERT) let mode_cesar (proof : #GText.view_skel) = function @@ -129,7 +129,7 @@ let display mode (view : #GText.view_skel) goals hints evars = match goals with | None -> () (* No proof in progress *) - | Some { Proof.fg_goals = []; bg_goals = bg; shelved_goals; given_up_goals; } -> + | Some { Interface.fg_goals = []; bg_goals = bg; shelved_goals; given_up_goals; } -> let bg = flatten (List.rev bg) in let evars = match evars with None -> [] | Some evs -> evs in begin match (bg, shelved_goals,given_up_goals, evars) with @@ -168,7 +168,7 @@ let display mode (view : #GText.view_skel) goals hints evars = in List.iter iter bg end - | Some { Proof.fg_goals = fg } -> + | Some { Interface.fg_goals = fg } -> mode view fg hints let proof_view () = |