Merge branch 'cerrors-cclosure' into trunk

Was PR#226: CErrors & CClosure

7 files changed, 8 insertions, 8 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 94981d0e1f..52f22ee603 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -13,7 +13,7 @@ open Names
 open Libnames
 open Globnames
 open Pp
-open Errors
+open CErrors
 open Util
 open Table
 open Extraction
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 4308b46338..312c2eab3d 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -684,7 +684,7 @@ and extract_cst_app env mle mlt kn u args =
 	let l,l' = List.chop (projection_arity (ConstRef kn)) mla in
 	if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
 	else mla
-      with e when Errors.noncritical e -> mla
+      with e when CErrors.noncritical e -> mla
   in
   (* For strict languages, purely logical signatures lead to a dummy lam
      (except when [Kill Ktype] everywhere). So a [MLdummy] is left
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 764223621e..0692c88cd1 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -9,7 +9,7 @@
 (*s Production of Haskell syntax. *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index bd48311308..864d90a0f2 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -8,7 +8,7 @@
 
 open Names
 open Globnames
-open Errors
+open CErrors
 open Util
 open Miniml
 open Table
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 3cb3810cbc..1c29a9bc24 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -9,7 +9,7 @@
 (*s Production of Ocaml syntax. *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops
@@ -203,7 +203,7 @@ let rec pp_expr par env args =
 	   let args = List.skipn (projection_arity r) args in
 	   let record = List.hd args in
 	   pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
-	 with e when Errors.noncritical e -> apply (pp_global Term r))
+	 with e when CErrors.noncritical e -> apply (pp_global Term r))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
 	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 7b0f14dff7..a6309e61f9 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -9,7 +9,7 @@
 (*s Production of Scheme syntax. *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Miniml
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 3a9ecc9ff9..ff66d915f5 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -15,7 +15,7 @@ open Libobject
 open Goptions
 open Libnames
 open Globnames
-open Errors
+open CErrors
 open Util
 open Pp
 open Miniml