diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.ml | 5 | ||||
| -rw-r--r-- | proofs/logic.ml | 22 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 11 | ||||
| -rw-r--r-- | proofs/tactic_debug.ml | 14 |
4 files changed, 29 insertions, 23 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index c8cb1d1cc2..9b358210a0 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -12,6 +12,7 @@ open Names open Evd open Evarutil open Evarsolve +open Pp (******************************************) (* Instantiation of existential variables *) @@ -54,8 +55,8 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = with e when Errors.noncritical e -> let loc = Glob_ops.loc_of_glob_constr rawc in user_err_loc - (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^ - string_of_existential evk)) + (loc,"", str "Instance is not well-typed in the environment of " ++ + str (string_of_existential evk)) in define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma) diff --git a/proofs/logic.ml b/proofs/logic.ml index b8206ca1b5..898588d9e4 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -179,7 +179,8 @@ let check_decl_position env sign (x,_,_ as d) = let needed = global_vars_set_of_decl env d in let deps = dependency_closure env (named_context_of_val sign) needed in if Id.List.mem x deps then - error ("Cannot create self-referring hypothesis "^Id.to_string x); + errorlabstrm "Logic.check_decl_position" + (str "Cannot create self-referring hypothesis " ++ pr_id x); x::deps (* Auxiliary functions for primitive MOVE tactic @@ -488,9 +489,11 @@ let convert_hyp check sign sigma (id,b,bt as d) = (fun _ (_,c,ct) _ -> let env = Global.env_of_context sign in if check && not (is_conv env sigma bt ct) then - error ("Incorrect change of the type of "^(Id.to_string id)^"."); + errorlabstrm "Logic.convert_hyp" + (str "Incorrect change of the type of " ++ pr_id id ++ str "."); if check && not (Option.equal (is_conv env sigma) b c) then - error ("Incorrect change of the body of "^(Id.to_string id)^"."); + errorlabstrm "Logic.convert_hyp" + (str "Incorrect change of the body of "++ pr_id id ++ str "."); if check then reorder := check_decl_position env sign d; d) in reorder_val_context env sign' !reorder @@ -522,7 +525,8 @@ let prim_refiner r sigma goal = t,cl,sigma else (if !check && mem_named_context id (named_context_of_val sign) then - error ("Variable " ^ Id.to_string id ^ " is already declared."); + errorlabstrm "Logic.prim_refiner" + (str "Variable " ++ pr_id id ++ str " is already declared."); push_named_context_val (id,None,t) sign,t,cl,sigma) in let (sg2,ev2,sigma) = Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in @@ -550,11 +554,10 @@ let prim_refiner r sigma goal = | (f,n,ar)::oth -> let ((sp',_),u') = check_ind env n ar in if not (eq_mind sp sp') then - error ("Fixpoints should be on the same " ^ - "mutual inductive declaration."); + error "Fixpoints should be on the same mutual inductive declaration."; if !check && mem_named_context f (named_context_of_val sign) then - error - ("Name "^Id.to_string f^" already used in the environment"); + errorlabstrm "Logic.prim_refiner" + (str "Name " ++ pr_id f ++ str " already used in the environment"); mk_sign (push_named_context_val (f,None,ar) sign) oth | [] -> Evd.Monad.List.map (fun (_,_,c) sigma -> @@ -584,8 +587,7 @@ let prim_refiner r sigma goal = try let _ = find_coinductive env sigma b in () with Not_found -> - error ("All methods must construct elements " ^ - "in coinductive types.") + error "All methods must construct elements in coinductive types." in let firsts,lasts = List.chop j others in let all = firsts@(f,cl)::lasts in diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 1383d75567..d25f7e9150 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -167,18 +167,20 @@ let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction" let declare_reduction s f = if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then error ("There is already a reduction expression of name "^s) + then errorlabstrm "Redexpr.declare_reduction" + (str "There is already a reduction expression of name " ++ str s) else reduction_tab := String.Map.add s f !reduction_tab let check_custom = function | ExtraRedExpr s -> if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab) - then error ("Reference to undefined reduction expression "^s) + then errorlabstrm "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s) |_ -> () let decl_red_expr s e = if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then error ("There is already a reduction expression of name "^s) + then errorlabstrm "Redexpr.decl_red_expr" + (str "There is already a reduction expression of name " ++ str s) else begin check_custom e; red_expr_tab := String.Map.add s e !red_expr_tab @@ -232,7 +234,8 @@ let reduction_of_red_expr env = with Not_found -> (try reduction_of_red_expr (String.Map.find s !red_expr_tab) with Not_found -> - error("unknown user-defined reduction \""^s^"\""))) + errorlabstrm "Redexpr.reduction_of_red_expr" + (str "unknown user-defined reduction \"" ++ str s ++ str "\""))) | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast) | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast) in diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 3cc81daf58..d7f4b5ead5 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -11,6 +11,7 @@ open Names open Pp open Tacexpr open Termops +open Nameops let (prtac, tactic_printer) = Hook.make () let (prmatchpatt, match_pattern_printer) = Hook.make () @@ -231,17 +232,16 @@ let db_pattern_rule debug num r = (* Prints the hypothesis pattern identifier if it exists *) let hyp_bound = function - | Anonymous -> " (unbound)" - | Name id -> " (bound to "^(Names.Id.to_string id)^")" + | Anonymous -> str " (unbound)" + | Name id -> str " (bound to " ++ pr_id id ++ str ")" (* Prints a matched hypothesis *) let db_matched_hyp debug env (id,_,c) ido = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str "Hypothesis " ++ - str ((Names.Id.to_string id)^(hyp_bound ido)^ - " has been matched: ") ++ print_constr_env env c) + msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++ + str " has been matched: " ++ print_constr_env env c) else return () (* Prints the matched conclusion *) @@ -266,8 +266,8 @@ let db_hyp_pattern_failure debug env sigma (na,hyp) = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str ("The pattern hypothesis"^(hyp_bound na)^ - " cannot match: ") ++ + msg_tac_debug (str "The pattern hypothesis" ++ hyp_bound na ++ + str " cannot match: " ++ Hook.get prmatchpatt env sigma hyp) else return () |