diff options
| author | aspiwack | 2011-02-10 10:10:58 +0000 |
|---|---|---|
| committer | aspiwack | 2011-02-10 10:10:58 +0000 |
| commit | ac776b4660e95577eb6742200d882b8cf683cc10 (patch) | |
| tree | 40cd96020ddd0a3f23f2580c2921d27001186161 /toplevel | |
| parent | daf397883f9b7f79eeddc6cc4580ecdc5ec793f5 (diff) | |
Started to fix the declarative proof mode (C-zar).
Everything seems to work fine in CoqIDE (except escape/return and the daimon which are not entirely ported).
However, there is some problem causing proof general to fail when using goto or evaluate buffer (evaluate next phrase works fine though), as well as coqc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13817 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f4fc8714be..ccbaa6d306 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -670,7 +670,7 @@ let pop_bullet pr = b | [] -> Util.anomaly "Tried to pop bullet from an empty stack" let push_bullet b pr = - Proof.focus bullet_cond 1 pr ; + Proof.focus bullet_cond () 1 pr ; set_bullets (b::get_bullets pr) pr let put_bullet p bul = @@ -690,10 +690,7 @@ let vernac_solve n bullet tcom b = solve_nth n (Tacinterp.hide_interp tcom None) ~with_end_tac:b; (* in case a strict subtree was completed, go back to the top of the prooftree *) - begin try while Proof.no_focused_goal p do - Proof.unfocus command_focus p - done - with Util.UserError _ -> () end; + Proof_global.maximal_unfocus command_focus p; print_subgoals(); if !pcoq <> None then (Option.get !pcoq).solve n @@ -1252,8 +1249,8 @@ let vernac_backtrack snum pnum naborts = let vernac_focus gln = let p = Proof_global.give_me_the_proof () in match gln with - | None -> Proof.focus focus_command_cond 1 p; print_subgoals () - | Some n -> Proof.focus focus_command_cond n p; print_subgoals () + | None -> Proof.focus focus_command_cond () 1 p; print_subgoals () + | Some n -> Proof.focus focus_command_cond () n p; print_subgoals () (* Unfocuses one step in the focus stack. *) @@ -1273,8 +1270,8 @@ let subproof_cond = Proof.done_cond subproof_kind let vernac_subproof gln = let p = Proof_global.give_me_the_proof () in begin match gln with - | None -> Proof.focus subproof_cond 1 p - | Some n -> Proof.focus subproof_cond n p + | None -> Proof.focus subproof_cond () 1 p + | Some n -> Proof.focus subproof_cond () n p end ; print_subgoals () |