diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-27 18:15:07 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2016-07-03 12:16:24 +0200 |
| commit | 3ce70f21a18cc19e720e8ac54b93652527881942 (patch) | |
| tree | c07c40d207b60b9c31fc148fc720b3890deb7f56 /plugins | |
| parent | cf95f2a791c263c7aaa3b488d1b09eaafc29be2b (diff) | |
rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cErrors.ml)
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
5 files changed, 6 insertions, 6 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 215c850b6..b0ffc775b 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -27,7 +27,7 @@ let observe strm = let do_observe_tac s tac g = try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v with e -> - let e = Cerrors.process_vernac_interp_error e in + let e = ExplainErr.process_vernac_interp_error e in let goal = begin try (Printer.pr_goal g) with _ -> assert false end in msg_debug (str "observation "++ s++str " raised exception " ++ Errors.print e ++ str " on goal " ++ goal ); @@ -76,7 +76,7 @@ let do_observe_tac s tac g = with reraise -> let reraise = CErrors.push reraise in if not (Stack.is_empty debug_queue) - then print_debug_queue (Some (fst (Cerrors.process_vernac_interp_error reraise))); + then print_debug_queue (Some (fst (ExplainErr.process_vernac_interp_error reraise))); iraise reraise let observe_tac_stream s tac g = diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 85897ecee..42e490315 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -195,7 +195,7 @@ END let warning_error names e = - let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in + let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> let names = pr_enum Libnames.pr_reference names in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 6e33af8fb..18817f504 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -225,7 +225,7 @@ let prepare_body ((name,_,args,types,_),_) rt = (fun_args,rt') let process_vernac_interp_error e = - fst (Cerrors.process_vernac_interp_error (e, Exninfo.null)) + fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null)) let warn_funind_cannot_build_inversion = CWarnings.create ~name:"funind-cannot-build-inversion" ~category:"funind" diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index e0c60d6d5..26fc88a60 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -72,7 +72,7 @@ let do_observe_tac s tac g = msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v with reraise -> let reraise = CErrors.push reraise in - let e = Cerrors.process_vernac_interp_error reraise in + let e = ExplainErr.process_vernac_interp_error reraise in observe (hov 0 (str "observation "++ s++str " raised exception " ++ CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal )); iraise reraise;; diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 027fe5677..62f307115 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -240,7 +240,7 @@ let do_observe_tac s tac g = with reraise -> let reraise = CErrors.push reraise in if not (Stack.is_empty debug_queue) - then print_debug_queue true (fst (Cerrors.process_vernac_interp_error reraise)); + then print_debug_queue true (fst (ExplainErr.process_vernac_interp_error reraise)); iraise reraise let observe_tac s tac g = |