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 /toplevel | |
| parent | cf95f2a791c263c7aaa3b488d1b09eaafc29be2b (diff) | |
rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cErrors.ml)
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/explainErr.ml (renamed from toplevel/cerrors.ml) | 0 | ||||
| -rw-r--r-- | toplevel/explainErr.mli (renamed from toplevel/cerrors.mli) | 0 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 4 | ||||
| -rw-r--r-- | toplevel/toplevel.mllib | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
6 files changed, 5 insertions, 5 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/explainErr.ml index 17897460c..17897460c 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/explainErr.ml diff --git a/toplevel/cerrors.mli b/toplevel/explainErr.mli index a67c887af..a67c887af 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/explainErr.mli diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 1be5226de..1f1be243e 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -872,7 +872,7 @@ let obligation_terminator name num guard hook auto pf = end with e when CErrors.noncritical e -> let e = CErrors.push e in - pperror (CErrors.iprint (Cerrors.process_vernac_interp_error e)) + pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) let obligation_hook prg obl num auto ctx' _ gr = let obls, rem = prg.prg_obligations in @@ -903,7 +903,7 @@ in try ignore (update_obls prg obls (pred rem)) with e when CErrors.noncritical e -> let e = CErrors.push e in - pperror (CErrors.iprint (Cerrors.process_vernac_interp_error e)) + pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) in if pred rem > 0 then begin let deps = dependencies obls num in diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index 5aa7d428a..d68922363 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -1,5 +1,5 @@ Himsg -Cerrors +ExplainErr Class Locality Metasyntax diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 3423a8b8c..0559934ec 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -378,4 +378,4 @@ let compile v f = CoqworkmgrApi.giveback 1 let () = Hook.set Stm.process_error_hook - Cerrors.process_vernac_interp_error + ExplainErr.process_vernac_interp_error diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index e4a2ca5a0..f69c4fa18 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -2009,7 +2009,7 @@ let with_fail b f = | e -> let e = CErrors.push e in raise (HasFailed (CErrors.iprint - (Cerrors.process_vernac_interp_error ~allow_uncaught:false ~with_header:false e)))) + (ExplainErr.process_vernac_interp_error ~allow_uncaught:false ~with_header:false e)))) () with e when CErrors.noncritical e -> let (e, _) = CErrors.push e in |