diff options
Diffstat (limited to 'plugins/funind')
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 | ||||
-rw-r--r-- | plugins/funind/g_indfun.ml4 | 4 | ||||
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 10 | ||||
-rw-r--r-- | plugins/funind/invfun.ml | 2 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 4 |
6 files changed, 13 insertions, 13 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 4f32bbd99..21ee32539 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -36,7 +36,7 @@ let do_observe_tac s tac g = with e -> let goal = begin try (Printer.pr_goal g) with _ -> assert false end in msgnl (str "observation "++ s++str " raised exception " ++ - Cerrors.explain_exn e ++ str " on goal " ++ goal ); + Errors.print e ++ str " on goal " ++ goal ); raise e;; let observe_tac_stream s tac g = @@ -608,7 +608,7 @@ let my_orelse tac1 tac2 g = try tac1 g with e -> -(* observe (str "using snd tac since : " ++ Cerrors.explain_exn e); *) +(* observe (str "using snd tac since : " ++ Errors.print e); *) tac2 g let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id = diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 39f4cf07f..53ddfb967 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -180,12 +180,12 @@ let warning_error names e = Pp.msg_warning (str "Cannot define graph(s) for " ++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++ - if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()) + if do_observe () then (spc () ++ Errors.print e) else mt ()) | Defining_principle e -> Pp.msg_warning (str "Cannot define principle(s) for "++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++ - if do_observe () then Cerrors.explain_exn e else mt ()) + if do_observe () then Errors.print e else mt ()) | _ -> raise e diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 394417abb..6d4e8929a 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1404,7 +1404,7 @@ let do_build_inductive str "while trying to define"++ spc () ++ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds)) ++ fnl () ++ - Cerrors.explain_exn e + Errors.print e in observe msg; raise e diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index dd48765fb..d98960a48 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -254,14 +254,14 @@ let derive_inversion fix_names = with e -> msg_warning (str "Cannot built inversion information" ++ - if do_observe () then Cerrors.explain_exn e else mt ()) + if do_observe () then Errors.print e else mt ()) with _ -> () let warning_error names e = let e_explain e = match e with - | ToShow e -> spc () ++ Cerrors.explain_exn e - | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt () + | ToShow e -> spc () ++ Errors.print e + | _ -> if do_observe () then (spc () ++ Errors.print e) else mt () in match e with | Building_graph e -> @@ -279,8 +279,8 @@ let warning_error names e = let error_error names e = let e_explain e = match e with - | ToShow e -> spc () ++ Cerrors.explain_exn e - | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt () + | ToShow e -> spc () ++ Errors.print e + | _ -> if do_observe () then (spc () ++ Errors.print e) else mt () in match e with | Building_graph e -> diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 426b496dd..1b7a19029 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -64,7 +64,7 @@ let do_observe_tac s tac g = let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v with e -> msgnl (str "observation "++ s++str " raised exception " ++ - Cerrors.explain_exn e ++ str " on goal " ++ goal ); + Errors.print e ++ str " on goal " ++ goal ); raise e;; diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 11fbc01ba..5b689625b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -75,7 +75,7 @@ let rec print_debug_queue b e = begin let lmsg,goal = Stack.pop debug_queue in if b then - msgnl (lmsg ++ (str " raised exception " ++ Cerrors.explain_exn e) ++ str " on goal " ++ goal) + msgnl (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal) else begin msgnl (str " from " ++ lmsg ++ str " on goal " ++ goal); @@ -1433,7 +1433,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num with e -> begin if Tacinterp.get_debug () <> Tactic_debug.DebugOff - then pperrnl (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e) + then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e) else anomaly "Cannot create equation Lemma" ; (* ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *) |