diff options
Diffstat (limited to 'plugins/funind')
| -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 |
4 files changed, 15 insertions, 15 deletions
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) () ; |