From 80f2f9462205193885f054338ab28bfcd17de965 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Sat, 2 Nov 2013 15:35:11 +0000 Subject: 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 --- plugins/funind/recdef.ml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'plugins/funind/recdef.ml') diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 76095cb1c..881d930fc 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1319,10 +1319,10 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ hook; if Indfun_common.is_strict_tcc () then - by (Proofview.V82.tactic (tclIDTAC)) + ignore (by (Proofview.V82.tactic (tclIDTAC))) else begin - by (Proofview.V82.tactic begin + ignore (by (Proofview.V82.tactic begin fun g -> tclTHEN (decompose_and_tac) @@ -1338,10 +1338,10 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ ) using_lemmas) ) tclIDTAC) - g end) + g end)) end; try - by (Proofview.V82.tactic tclIDTAC); (* raises UserError _ if the proof is complete *) + ignore (by (Proofview.V82.tactic tclIDTAC)); (* raises UserError _ if the proof is complete *) with UserError _ -> defined () @@ -1364,9 +1364,9 @@ let com_terminate (Global, Proof Lemma) (Environ.named_context_val env) (compute_terminate_type nb_args fonctional_ref) hook; - by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start)); - by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref - input_type relation rec_arg_num ))) + ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start))); + ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref + input_type relation rec_arg_num )))) in start_proof tclIDTAC tclIDTAC; try @@ -1410,7 +1410,7 @@ let (com_eqn : int -> Id.t -> let equation_lemma_type = subst1 f_constr equation_lemma_type in (start_proof eq_name (Global, Proof Lemma) (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ()); - by + ignore (by (Proofview.V82.tactic (start_equation f_ref terminate_ref (fun x -> prove_eq (fun _ -> tclIDTAC) @@ -1437,7 +1437,7 @@ let (com_eqn : int -> Id.t -> ih = Id.of_string "______"; } ) - )); + ))); (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *) (* Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *) Flags.silently (fun () -> Lemmas.save_named opacity) () ; -- cgit v1.2.3