diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 6 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 8 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 18 |
6 files changed, 20 insertions, 20 deletions
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index f3c5da2ad2..cbdcc96aa9 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -100,13 +100,13 @@ let proof_cond = Proof.no_cond proof_focus let focus p = let inf = get_stack p in - Proof_global.with_current_proof (fun _ -> Proof.focus proof_cond inf 1) + Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1) let unfocus () = - Proof_global.with_current_proof (fun _ p -> Proof.unfocus proof_focus p ()) + Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ()) let maximal_unfocus () = - Proof_global.with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus) + Proof_global.simple_with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus) let get_top_stack pts = try diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index e47776bd7d..6b5cb7492b 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -121,7 +121,7 @@ let start_proof_tac gls= tcl_change_info info gls let go_to_proof_mode () = - Pfedit.by (Proofview.V82.tactic start_proof_tac); + ignore (Pfedit.by (Proofview.V82.tactic start_proof_tac)); let p = Proof_global.give_me_the_proof () in Decl_mode.focus p @@ -1461,7 +1461,7 @@ let do_instr raw_instr pts = let glob_instr = intern_proof_instr ist raw_instr in let instr = interp_proof_instr (get_its_info gl) sigma env glob_instr in - Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)) + ignore (Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp))) else () end; postprocess pts raw_instr.instr; (* spiwack: this should restore a compatible semantics with diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 2da4b61478..8c2fdb7eb5 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -983,7 +983,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) lemma_type (fun _ _ -> ()); - Pfedit.by (Proofview.V82.tactic prove_replacement); + ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); Lemmas.save_named false diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 0850d556cc..3d577b4401 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -297,7 +297,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro (hook new_principle_type) ; (* let _tim1 = System.get_time () in *) - Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map mkConst funs) mutr_nparams)); + ignore (Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map mkConst funs) mutr_nparams))); (* let _tim2 = System.get_time () in *) (* begin *) (* let dur1 = System.time_difference tim1 tim2 in *) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ce25f7aaf0..36de855957 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1069,9 +1069,9 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i)) (fun _ _ -> ()); - Pfedit.by + ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") - (proving_tac i))); + (proving_tac i)))); do_save (); let finfo = find_Function_infos f_as_constant in let lem_cst = destConst (Constrintern.global_reference lem_id) in @@ -1120,9 +1120,9 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i)) (fun _ _ -> ()); - Pfedit.by + ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") - (proving_tac i))); + (proving_tac i)))); do_save (); let finfo = find_Function_infos f_as_constant in let lem_cst = destConst (Constrintern.global_reference lem_id) in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 76095cb1c8..881d930fcc 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) () ; |