From f9580dfa7bc89d0ca4c9d8b69d5f4b42d558234e Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 15 Apr 2015 13:51:38 +0200 Subject: Remove dirty debug printing from funind. --- plugins/funind/invfun.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d9ae87ecc1..d10924f886 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -378,7 +378,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres))); (* Conclusion *) observe_tac "exact" (fun g -> - Pp.msgnl (str "TITI " ++ pf_apply Printer.pr_lconstr_env g (app_constructor g)); Proofview.V82.of_tactic (exact_check (app_constructor g)) g) ] ) @@ -427,7 +426,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes in (params_bindings@lemmas_bindings) in - Pp.msgnl (str "princ_type := " ++ pf_apply Printer.pr_lconstr_env g princ_type); tclTHENSEQ [ observe_tac "principle" (Proofview.V82.of_tactic (assert_by -- cgit v1.2.3 From b4552eb74c7ee577339b44924b59c2ab25f893d2 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 22 Apr 2015 13:29:46 +0200 Subject: Declarative mode: remaining goals are "given up" when closing blocks. Restores the intended behaviour from v8.3 and earlier.--- plugins/decl_mode/decl_proof_instr.ml | 30 +++++++++++++++++++++++++++--- 1 file changed, 27 insertions(+), 3 deletions(-) (limited to 'plugins') diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 9d0b7f3466..36273faae2 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -125,10 +125,34 @@ let go_to_proof_mode () = (* closing gaps *) +(* spiwack: should use [Proofview.give_up] but that would require + moving the whole declarative mode into the new proof engine. It + will eventually have to be done. + + As far as I can tell, [daimon_tac] is used after a [thus thesis], + it will leave uninstantiated variables instead of giving a relevant + message at [Qed]. *) let daimon_tac gls = set_daimon_flag (); {it=[];sigma=sig_sig gls;} +let daimon_instr env p = + let (p,(status,_)) = + Proof.run_tactic env begin + Proofview.tclINDEPENDENT Proofview.give_up + end p + in + p,status + +let do_daimon () = + let env = Global.env () in + let status = + Proof_global.with_current_proof begin fun _ p -> + daimon_instr env p + end + in + if not status then Pp.feedback Feedback.AddedAxiom else () + (* post-instruction focus management *) let goto_current_focus () = @@ -144,7 +168,7 @@ let goto_current_focus_or_top () = (* return *) let close_tactic_mode () = - try goto_current_focus () + try do_daimon ();goto_current_focus () with Not_found -> error "\"return\" cannot be used outside of Declarative Proof Mode." @@ -165,7 +189,7 @@ let close_block bt pts = in match bt,stack with B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> - (goto_current_focus ()) + do_daimon ();goto_current_focus () | _, Claim::_ -> error "\"end claim\" expected." | _, Focus_claim::_ -> @@ -196,7 +220,7 @@ let close_previous_case pts = match get_stack pts with Per (et,_,_,_) :: _ -> () | Suppose_case :: Per (et,_,_,_) :: _ -> - goto_current_focus () + do_daimon ();goto_current_focus () | _ -> error "Not inside a proof per cases or induction." (* Proof instructions *) -- cgit v1.2.3 From 915c8f15965fe8e7ee9d02a663fd890ef80539ad Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 23 Apr 2015 14:22:42 +0200 Subject: Using tclZEROMSG instead of tclZERO in several places. --- plugins/cc/cctac.ml | 4 ++-- plugins/omega/coq_omega.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins') diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 8884aef1cf..05f4c49030 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -302,9 +302,9 @@ let rec proof_tac p : unit Proofview.tactic = Tacticals.New.tclFIRST [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2); reflexivity; - Proofview.tclZERO (UserError ("Congruence" , + Tacticals.New.tclZEROMSG (Pp.str - "I don't know how to handle dependent equality")))]] + "I don't know how to handle dependent equality")]] | Inject (prf,cstr,nargs,argind) -> let ti=constr_of_term prf.p_lhs in let tj=constr_of_term prf.p_rhs in diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 37428c39da..4e2696dfdb 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1462,7 +1462,7 @@ let coq_omega = let path = simplify_strong (new_id,new_var_num,display_var) system in if !display_action_flag then display_action display_var path; Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path) - with NO_CONTRADICTION -> Proofview.tclZERO (UserError ("" , Pp.str"Omega can't solve this system")) + with NO_CONTRADICTION -> Tacticals.New.tclZEROMSG (Pp.str"Omega can't solve this system") end end -- cgit v1.2.3 From 16d301bab5b7dec53be4786b3b6815bca54ae539 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 23 Apr 2015 14:55:11 +0200 Subject: Remove almost all the uses of string concatenation when building error messages. Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure. --- plugins/funind/functional_principles_types.ml | 13 ++++++++----- plugins/funind/indfun_common.ml | 4 +++- plugins/funind/recdef.ml | 3 ++- 3 files changed, 13 insertions(+), 7 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 45e5aaf545..a2bbf97ae3 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -604,7 +604,8 @@ let build_scheme fas = try Smartlocate.global_with_alias f with Not_found -> - Errors.error ("Cannot find "^ Libnames.string_of_reference f) + errorlabstrm "FunInd.build_scheme" + (str "Cannot find " ++ Libnames.pr_reference f) in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' f in @@ -636,10 +637,12 @@ let build_case_scheme fa = (* let id_to_constr id = *) (* Constrintern.global_reference id *) (* in *) - let funs = (fun (_,f,_) -> - try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f)) - with Not_found -> - Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in + let funs = + let (_,f,_) = fa in + try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f)) + with Not_found -> + errorlabstrm "FunInd.build_case_scheme" + (str "Cannot find " ++ Libnames.pr_reference f) in let first_fun,u = destConst funs in let funs_mp,funs_dp,_ = Names.repr_con first_fun in let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 738ade8ca3..1c409500ef 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -109,7 +109,9 @@ let const_of_id id = qualid_of_reference (Libnames.Ident (Loc.ghost,id)) in try Constrintern.locate_reference princ_ref - with Not_found -> Errors.error ("cannot find "^ Id.to_string id) + with Not_found -> + Errors.errorlabstrm "IndFun.const_of_id" + (str "cannot find " ++ Nameops.pr_id id) let def_of_const t = match (Term.kind_of_term t) with diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 0999b95d71..b9902a9fc7 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -305,7 +305,8 @@ let check_not_nested forbidden e = | Rel _ -> () | Var x -> if Id.List.mem x forbidden - then error ("check_not_nested : failure "^Id.to_string x) + then errorlabstrm "Recdef.check_not_nested" + (str "check_not_nested: failure " ++ pr_id x) | Meta _ | Evar _ | Sort _ -> () | Cast(e,_,t) -> check_not_nested e;check_not_nested t | Prod(_,t,b) -> check_not_nested t;check_not_nested b -- cgit v1.2.3