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

6 files changed, 19 insertions, 20 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a383b14528..9edf6302da 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -785,5 +785,5 @@ END;;
 VERNAC COMMAND EXTEND GrabEvars
 [ "Grab" "Existential" "Variables" ]
   => [ Vernacexpr.VtProofStep, Vernacexpr.VtLater ]
-  -> [ Proof_global.with_current_proof (fun _ p  -> Proof.V82.grab_evars p) ]
+  -> [ Proof_global.simple_with_current_proof (fun _ p  -> Proof.V82.grab_evars p) ]
 END
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index f889f9cb2c..846bba1d46 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -146,21 +146,20 @@ TACTIC EXTEND setoid_rewrite
       [ Proofview.V82.tactic (cl_rewrite_clause c o (occurrences_of occ) (Some id))]
 END
 
-let cl_rewrite_clause_newtac_tac c o occ cl gl =
-  cl_rewrite_clause_newtac' c o occ cl;
-  tclIDTAC gl
+let cl_rewrite_clause_newtac_tac c o occ cl =
+  cl_rewrite_clause_newtac' c o occ cl
 
 TACTIC EXTEND GenRew
 | [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ) ] ->
-    [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id)) ]
+    [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id) ]
 | [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id) ] ->
-    [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id)) ]
+    [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id) ]
 | [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] ->
-    [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o AllOccurrences (Some id)) ]
+    [ cl_rewrite_clause_newtac_tac c o AllOccurrences (Some id) ]
 | [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] ->
-    [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o (occurrences_of occ) None) ]
+    [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) None ]
 | [ "rew" orient(o) glob_constr_with_bindings(c) ] ->
-    [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o AllOccurrences None) ]
+    [ cl_rewrite_clause_newtac_tac c o AllOccurrences None ]
 END
 
 VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 06b067fcf4..04819830e5 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -198,8 +198,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   *)
   let pf = Proof.start [invEnv,invGoal] in
   let pf =
-    Proof.run_tactic env (
-      Tacticals.New.tclTHEN intro (Tacticals.New.onLastHypId inv_op)) pf
+    fst (Proof.run_tactic env (
+      Tacticals.New.tclTHEN intro (Tacticals.New.onLastHypId inv_op)) pf)
   in
   let pfterm = List.hd (Proof.partial_proof pf) in
   let global_named_context = Global.named_context () in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 30fe8d4aef..66b2c64b0f 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -361,7 +361,7 @@ let solve_remaining_by by env prf =
     let evd' = 
       List.fold_right (fun mv evd ->
         let ty = Clenv.clenv_nf_meta env (meta_type evd mv) in
-	let c = Pfedit.build_by_tactic env.env ty (Tacticals.New.tclCOMPLETE tac) in
+	let c,_ = Pfedit.build_by_tactic env.env ty (Tacticals.New.tclCOMPLETE tac) in
 	  meta_assign mv (c, (Conv,TypeNotProcessed)) evd)
       indep env.evd
     in { env with evd = evd' }, prf
@@ -1342,9 +1342,8 @@ let cl_rewrite_clause_new_strat ?abs strat clause =
    newfail 0 (str"setoid rewrite failed: " ++ s))
 
 let cl_rewrite_clause_newtac' l left2right occs clause =
-  Proof_global.with_current_proof (fun _ -> Proof.run_tactic (Global.env ())
-    (Proofview.tclFOCUS 1 1 
-       (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause)))
+  Proofview.tclFOCUS 1 1 
+       (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause)
 
 let cl_rewrite_clause_strat strat clause =
   tclTHEN (tactic_init_setoid ())
@@ -1641,7 +1640,7 @@ let add_morphism_infer glob m n =
 				   glob (ConstRef cst));
 		  declare_projection n instance_id (ConstRef cst)
 		| _ -> assert false);
-	    Pfedit.by (Tacinterp.interp tac)) ()
+	    ignore (Pfedit.by (Tacinterp.interp tac))) ()
 
 let add_morphism glob binders m s n =
   init_setoid ();
diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli
index 637bab5a6a..63166c64a5 100644
--- a/tactics/rewrite.mli
+++ b/tactics/rewrite.mli
@@ -43,7 +43,7 @@ val cl_rewrite_clause :
 
 val cl_rewrite_clause_newtac' :
   interp_sign * (glob_constr_and_expr * glob_constr_and_expr bindings) ->
-  bool -> Locus.occurrences -> Id.t option -> unit
+  bool -> Locus.occurrences -> Id.t option -> unit Proofview.tactic
 
 val is_applied_rewrite_relation :
   env -> evar_map -> Context.rel_context -> constr -> types option
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5b1ae69e33..4026b42587 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3740,7 +3740,8 @@ let abstract_subproof id tac gl =
     try flush_and_check_evars (project gl) concl
     with Uninstantiated_evar _ ->
       error "\"abstract\" cannot handle existentials." in
-  let const = Pfedit.build_constant_by_tactic id secsign concl
+  (* spiwack: the [abstract] tacticals loses the "unsafe status" information *)
+  let (const,_) = Pfedit.build_constant_by_tactic id secsign concl
     (Tacticals.New.tclCOMPLETE (Tacticals.New.tclTHEN (Tacticals.New.tclDO (List.length sign) intro) tac)) in
   let cd = Entries.DefinitionEntry const in
   let decl = (cd, IsProof Lemma) in
@@ -3764,9 +3765,9 @@ let tclABSTRACT name_op tac gl =
 
 
 let admit_as_an_axiom =
-  (* spiwack: admit temporarily won't report an unsafe status *)
   Proofview.tclUNIT () >= fun () -> (* delay for Coqlib.build_coq_proof_admitted *)
-  simplest_case (Coqlib.build_coq_proof_admitted ())
+  simplest_case (Coqlib.build_coq_proof_admitted ()) <*>
+  Proofview.mark_as_unsafe
 
 let unify ?(state=full_transparent_state) x y gl =
   try