diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 12 | ||||
| -rw-r--r-- | toplevel/classes.ml | 7 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 5 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 26 |
4 files changed, 27 insertions, 23 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index f35a34633..50d013044 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -626,8 +626,8 @@ let make_bl_scheme mind = let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in - [|Pfedit.build_by_tactic (Global.env()) bl_goal - (compute_bl_tact (!bl_scheme_kind_aux()) ind lnamesparrec nparrec)|], + [|fst (Pfedit.build_by_tactic (Global.env()) bl_goal + (compute_bl_tact (!bl_scheme_kind_aux()) ind lnamesparrec nparrec))|], eff let bl_scheme_kind = declare_mutual_scheme_object "_dec_bl" make_bl_scheme @@ -741,8 +741,8 @@ let make_lb_scheme mind = let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in - [|Pfedit.build_by_tactic (Global.env()) lb_goal - (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)|], + [|fst (Pfedit.build_by_tactic (Global.env()) lb_goal + (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec))|], eff let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme @@ -903,9 +903,9 @@ let make_eq_decidability mind = let nparrec = mib.mind_nparams_rec in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in - [|Pfedit.build_by_tactic (Global.env()) + [|fst (Pfedit.build_by_tactic (Global.env()) (compute_dec_goal ind lnamesparrec nparrec) - (compute_dec_tact ind lnamesparrec nparrec)|], Declareops.no_seff + (compute_dec_tact ind lnamesparrec nparrec))|], Declareops.no_seff let eq_dec_scheme_kind = declare_mutual_scheme_object "_eq_dec" make_eq_decidability diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 121f8f4e1..728baadb4 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -298,11 +298,12 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props (fun () -> Lemmas.start_proof id kind termtype (fun _ -> instance_hook k pri global imps ?hook); + (* spiwack: I don't know what to do with the status here. *) if not (Option.is_empty term) then - Pfedit.by (!refine_ref (evm, Option.get term)) + ignore (Pfedit.by (!refine_ref (evm, Option.get term))) else if Flags.is_auto_intros () then - Pfedit.by (Tacticals.New.tclDO len Tactics.intro); - (match tac with Some tac -> Pfedit.by tac | None -> ())) (); + ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro)); + (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) (); id) end) diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 13e12b7e1..3eb61ccdf 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -761,7 +761,8 @@ let rec string_of_list sep f = function (* Solve an obligation using tactics, return the corresponding proof term *) let solve_by_tac evi t = let id = Id.of_string "H" in - let entry = Pfedit.build_constant_by_tactic + (* spiwack: the status is dropped *) + let (entry,_) = Pfedit.build_constant_by_tactic id ~goal_kind evi.evar_hyps evi.evar_concl (Tacticals.New.tclCOMPLETE t) in let env = Global.env () in let entry = Term_typing.handle_side_effects env entry in @@ -814,7 +815,7 @@ let rec solve_obligation prg num tac = | _ -> ()); trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ Printer.pr_constr_env (Global.env ()) obl.obl_type); - Pfedit.by (snd (get_default_tactic ())); + ignore (Pfedit.by (snd (get_default_tactic ()))); Option.iter (fun tac -> Pfedit.set_end_tac tac) tac | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a0a355a15..62243781a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -475,8 +475,9 @@ let vernac_end_proof ?proof = function let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) - by (Tactics.New.exact_proof c); - save_named true + let status = by (Tactics.New.exact_proof c) in + save_named true; + if not status then Pp.feedback Interface.AddedAxiom let vernac_assumption locality (local, kind) l nl = let local = enforce_locality_exp locality local in @@ -774,15 +775,16 @@ let focus_command_cond = Proof.no_cond command_focus let vernac_solve n tcom b = if not (refining ()) then error "Unknown command of the non proof-editing mode."; - Proof_global.with_current_proof (fun etac p -> + let status = Proof_global.with_current_proof (fun etac p -> let with_end_tac = if b then Some etac else None in - let p = solve_nth n (Tacinterp.hide_interp tcom None) ?with_end_tac p in + let (p,status) = solve_nth n (Tacinterp.hide_interp tcom None) ?with_end_tac p in (* in case a strict subtree was completed, go back to the top of the prooftree *) let p = Proof.maximal_unfocus command_focus p in - p); - print_subgoals() -;; + p,status) in + print_subgoals(); + if not status then Pp.feedback Interface.AddedAxiom + (* A command which should be a tactic. It has been added by Christine to patch an error in the design of the proof @@ -1486,7 +1488,7 @@ let vernac_register id r = (* Proof management *) let vernac_focus gln = - Proof_global.with_current_proof (fun _ p -> + Proof_global.simple_with_current_proof (fun _ p -> match gln with | None -> Proof.focus focus_command_cond () 1 p | Some 0 -> @@ -1497,7 +1499,7 @@ let vernac_focus gln = (* Unfocuses one step in the focus stack. *) let vernac_unfocus () = - Proof_global.with_current_proof (fun _ p -> Proof.unfocus command_focus p ()); + Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus command_focus p ()); print_subgoals () (* Checks that a proof is fully unfocused. Raises an error if not. *) @@ -1519,19 +1521,19 @@ let subproof_kind = Proof.new_focus_kind () let subproof_cond = Proof.done_cond subproof_kind let vernac_subproof gln = - Proof_global.with_current_proof (fun _ p -> + Proof_global.simple_with_current_proof (fun _ p -> match gln with | None -> Proof.focus subproof_cond () 1 p | Some n -> Proof.focus subproof_cond () n p); print_subgoals () let vernac_end_subproof () = - Proof_global.with_current_proof (fun _ p -> Proof.unfocus subproof_kind p ()); + Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus subproof_kind p ()); print_subgoals () let vernac_bullet (bullet:Proof_global.Bullet.t) = - Proof_global.with_current_proof (fun _ p -> + Proof_global.simple_with_current_proof (fun _ p -> Proof_global.Bullet.put p bullet); (* Makes the focus visible in emacs by re-printing the goal. *) if !Flags.print_emacs then print_subgoals () |