The tactic [admit] exits with the "unsafe" status.

It is highlighted in yellow in Coqide.
The unsafe status is tracked throughout the execution of tactics such that
nested calls to admit are caught.

Many function (mainly those building constr with tactics such as typeclass
related stuff, and Function, and a few other like eauto's use of Hint Extern)
drop the unsafe status. This is unfortunate, but a lot of refactoring would
be in order.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16977 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 27 insertions, 23 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index f35a346335..50d0130445 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 121f8f4e1a..728baadb41 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 13e12b7e15..3eb61ccdf3 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 a0a355a154..62243781ae 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 ()