Merge branch 'cerrors-cclosure' into trunk

Was PR#226: CErrors & CClosure

11 files changed, 17 insertions, 17 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index f49ed9a5f4..04429851fd 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -382,18 +382,18 @@ let rec prod_constr_expr c = function
 let coerce_reference_to_id = function
   | Ident (_,id) -> id
   | Qualid (loc,_) ->
-      Errors.user_err_loc (loc, "coerce_reference_to_id",
+      CErrors.user_err_loc (loc, "coerce_reference_to_id",
         str "This expression should be a simple identifier.")
 
 let coerce_to_id = function
   | CRef (Ident (loc,id),_) -> (loc,id)
-  | a -> Errors.user_err_loc
+  | a -> CErrors.user_err_loc
         (constr_loc a,"coerce_to_id",
          str "This expression should be a simple identifier.")
 
 let coerce_to_name = function
   | CRef (Ident (loc,id),_) -> (loc,Name id)
   | CHole (loc,_,_,_) -> (loc,Anonymous)
-  | a -> Errors.user_err_loc
+  | a -> CErrors.user_err_loc
         (constr_loc a,"coerce_to_name",
          str "This expression should be a name.")
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 99b2292515..7476871890 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -8,7 +8,7 @@
 
 (*i*)
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 74de6f67ff..470eb83240 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops
@@ -779,7 +779,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
 	let scopes = find_arguments_scope ref in
 	Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
 	GRef (loc, ref, None), impls, scopes, []
-      with e when Errors.noncritical e ->
+      with e when CErrors.noncritical e ->
 	(* [id] a goal variable *)
 	GVar (loc,id), [], [], []
 
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 23bcddaea2..588637b76e 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Pp
 open Names
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index b50732e4e9..10cfbe58fa 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -9,7 +9,7 @@
 (*i*)
 open Names
 open Decl_kinds
-open Errors
+open CErrors
 open Util
 open Glob_term
 open Constrexpr
diff --git a/interp/notation.ml b/interp/notation.ml
index d42307040d..0798d385d4 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 (*i*)
-open Errors
+open CErrors
 open Util
 open Pp
 open Bigint
@@ -208,7 +208,7 @@ let remove_delimiters scope =
   let sc = find_scope scope in
   let newsc = { sc with delimiters = None } in
   match sc.delimiters with
-    | None -> Errors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".")
+    | None -> CErrors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".")
     | Some key ->
        scope_map := String.Map.add scope newsc !scope_map;
        try
@@ -1056,6 +1056,6 @@ let with_notation_protection f x =
   let fs = freeze false in
   try let a = f x in unfreeze fs; a
   with reraise ->
-    let reraise = Errors.push reraise in
+    let reraise = CErrors.push reraise in
     let () = unfreeze fs in
     iraise reraise
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index d8e022ce65..198bd2216a 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops
@@ -111,7 +111,7 @@ let rec eq_notation_constr t1 t2 = match t1, t2 with
 (* Re-interpret a notation as a glob_constr, taking care of binders   *)
 
 let name_to_ident = function
-  | Anonymous -> Errors.error "This expression should be a simple identifier."
+  | Anonymous -> CErrors.error "This expression should be a simple identifier."
   | Name id -> id
 
 let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 7e42c1a227..388ca08050 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -8,7 +8,7 @@
 
 (* Reserved names *)
 
-open Errors
+open CErrors
 open Util
 open Pp
 open Names
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 1f28ba6569..478774219e 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -13,7 +13,7 @@
 
 (* *)
 open Pp
-open Errors
+open CErrors
 open Libnames
 open Globnames
 open Misctypes
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 7170fd14a5..f96d8acc10 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Pp
 open Names
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 4109bdb7f5..2b860173a6 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -8,7 +8,7 @@
 
 (*i*)
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops