aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-27 11:03:43 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-03 12:08:03 +0200
commitf14b6f1a17652566f0cbc00ce81421ba0684dad5 (patch)
tree8a331593d0d1b518e8764c92ac54e3b11c222358 /printing
parent500d38d0887febb614ddcadebaef81e0c7942584 (diff)
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml2
-rw-r--r--printing/pptactic.ml2
-rw-r--r--printing/ppvernac.ml6
-rw-r--r--printing/prettyp.ml2
-rw-r--r--printing/printer.ml10
-rw-r--r--printing/printmod.ml8
6 files changed, 15 insertions, 15 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 1ea502539..252b0967d 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -7,7 +7,7 @@
(************************************************************************)
(*i*)
-open Errors
+open CErrors
open Util
open Pp
open Names
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 0ab1349ec..917a277c9 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -9,7 +9,7 @@
open Pp
open Names
open Namegen
-open Errors
+open CErrors
open Util
open Constrexpr
open Tacexpr
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 5b73b054d..0d47b34df 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -9,7 +9,7 @@
open Pp
open Names
-open Errors
+open CErrors
open Util
open Extend
open Vernacexpr
@@ -1082,7 +1082,7 @@ module Make
)
| VernacSetOpacity _ ->
return (
- Errors.anomaly (keyword "VernacSetOpacity used to set something else")
+ CErrors.anomaly (keyword "VernacSetOpacity used to set something else")
)
| VernacSetStrategy l ->
let pr_lev = function
@@ -1219,7 +1219,7 @@ module Make
let pr_vernac v =
try pr_vernac_body v ++ sep_end v
- with e -> Errors.print e
+ with e -> CErrors.print e
end
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index ad67becd0..1f6e99c7e 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -11,7 +11,7 @@
*)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
diff --git a/printing/printer.ml b/printing/printer.ml
index 0bac2755b..28fd92659 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -184,7 +184,7 @@ let safe_gen f env sigma c =
let orig_extern_ref = Constrextern.get_extern_reference () in
let extern_ref loc vars r =
try orig_extern_ref loc vars r
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
Libnames.Qualid (loc, qualid_of_global env r)
in
Constrextern.set_extern_reference extern_ref;
@@ -192,7 +192,7 @@ let safe_gen f env sigma c =
let p = f env sigma c in
Constrextern.set_extern_reference orig_extern_ref;
p
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
Constrextern.set_extern_reference orig_extern_ref;
str "??"
@@ -802,13 +802,13 @@ let pr_assumptionset env s =
in
let safe_pr_ltype typ =
try str " : " ++ pr_ltype typ
- with e when Errors.noncritical e -> mt ()
+ with e when CErrors.noncritical e -> mt ()
in
let safe_pr_ltype_relctx (rctx, typ) =
let sigma, env = get_current_context () in
let env = Environ.push_rel_context rctx env in
try str " " ++ pr_ltype_env env sigma typ
- with e when Errors.noncritical e -> mt ()
+ with e when CErrors.noncritical e -> mt ()
in
let pr_axiom env ax typ =
match ax with
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 5f98eeeab..c939f54e8 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -254,7 +254,7 @@ let nametab_register_modparam mbid mtb =
via a Declaremods function that converts back to module entries *)
try
Declaremods.process_module_binding mbid (get_typ_expr_alg mtb)
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
(* Otherwise, we try to play with the nametab ourselves *)
let mp = MPbound mbid in
let dir = DirPath.make [MBId.to_id mbid] in
@@ -295,7 +295,7 @@ let print_body is_impl env mp (l,body) =
try
let env = Option.get env in
pr_mutual_inductive_body env (MutInd.make2 mp l) mib
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
let keyword =
let open Decl_kinds in
match mib.mind_finite with
@@ -422,7 +422,7 @@ let print_module with_body mp =
try
if !short then raise ShortPrinting;
unsafe_print_module (Some (Global.env ())) mp with_body me ++ fnl ()
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
unsafe_print_module None mp with_body me ++ fnl ()
let print_modtype kn =
@@ -433,7 +433,7 @@ let print_modtype kn =
(try
if !short then raise ShortPrinting;
print_signature' true (Some (Global.env ())) kn mtb.mod_type
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
print_signature' true None kn mtb.mod_type))
end