Merge branch 'cerrors-cclosure' into trunk

Was PR#226: CErrors & CClosure

54 files changed, 187 insertions, 187 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index aee0bd8564..6e8b2eb0fb 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -212,7 +212,7 @@ module Btauto = struct
         let assign = List.map map_msg assign in
         let l = str "[" ++ (concat (str ";" ++ spc ()) assign) ++ str "]" in
         str "Not a tautology:" ++ spc () ++ l
-      with e when Errors.noncritical e -> (str "Not a tautology")
+      with e when CErrors.noncritical e -> (str "Not a tautology")
     in
     Tacticals.tclFAIL 0 msg gl
 
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 76db2f3c2f..bc53b113df 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -10,7 +10,7 @@
 (* Downey,Sethi and Tarjan. *)
 (* Plus some e-matching and constructor handling by P. Corbineau *)
 
-open Errors
+open CErrors
 open Util
 open Pp
 open Goptions
@@ -484,7 +484,7 @@ let build_subst uf subst =
   Array.map
     (fun i ->
       try term uf i
-      with e when Errors.noncritical e ->
+      with e when CErrors.noncritical e ->
         anomaly (Pp.str "incomplete matching"))
     subst
 
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index d2bbaf6a7d..f58847cafb 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -9,7 +9,7 @@
 (* This file uses the (non-compressed) union-find structure to generate *)
 (* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
 
-open Errors
+open CErrors
 open Term
 open Ccalgo
 open Pp
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index de64368e2f..aff60eaa4e 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -20,7 +20,7 @@ open Typing
 open Ccalgo
 open Ccproof
 open Pp
-open Errors
+open CErrors
 open Util
 open Proofview.Notations
 open Context.Rel.Declaration
@@ -38,12 +38,12 @@ let _True = reference ["Init";"Logic"] "True"
 let _I = reference ["Init";"Logic"] "I"
 
 let whd env=
-  let infos=Closure.create_clos_infos Closure.betaiotazeta env in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos CClosure.betaiotazeta env in
+    (fun t -> CClosure.whd_val infos (CClosure.inject t))
 
 let whd_delta env=
-   let infos=Closure.create_clos_infos Closure.all env in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
+   let infos=CClosure.create_clos_infos CClosure.all env in
+    (fun t -> CClosure.whd_val infos (CClosure.inject t))
 
 (* decompose member of equality in an applicative format *)
 
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index c0ef343059..a862423e99 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Constrexpr
@@ -153,8 +153,8 @@ let interp_constr check_sort env sigma c =
     fst (understand env sigma (fst c))
 
 let special_whd env =
-  let infos=Closure.create_clos_infos Closure.all env in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos CClosure.all env in
+    (fun t -> CClosure.whd_val infos (CClosure.inject t))
 
 let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq))
 
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index f9399d6824..92d4089015 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -9,7 +9,7 @@
 open Names
 open Term
 open Evd
-open Errors
+open CErrors
 open Util
 
 let daimon_flag = ref false
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index b6c34d2703..97c9d5f4a2 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Pp
 open Evd
@@ -84,12 +84,12 @@ let tcl_erase_info gls =
   tcl_change_info_gen info_gen gls
 
 let special_whd gl=
-  let infos=Closure.create_clos_infos Closure.all (pf_env gl) in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in
+    (fun t -> CClosure.whd_val infos (CClosure.inject t))
 
 let special_nf gl=
-  let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in
-    (fun t -> Closure.norm_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in
+    (fun t -> CClosure.norm_val infos (CClosure.inject t))
 
 let is_good_inductive env ind =
   let mib,oib = Inductive.lookup_mind_specif env ind in
@@ -277,7 +277,7 @@ let prepare_goal items gls =
        filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls
 
 let my_automation_tac = ref
-  (Proofview.tclZERO (Errors.make_anomaly (Pp.str"No automation registered")))
+  (Proofview.tclZERO (CErrors.make_anomaly (Pp.str"No automation registered")))
 
 let register_automation_tac tac = my_automation_tac:= tac
 
@@ -415,7 +415,7 @@ let find_subsubgoal c ctyp skip submetas gls =
 		  se.se_meta submetas se.se_meta_list}
 	  else
 	      dfs (pred n)
-      with e when Errors.noncritical e ->
+      with e when CErrors.noncritical e ->
 	begin
 	  enstack_subsubgoals env se stack gls;
 	  dfs n
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 73d3d1bab8..6c17dcc4f1 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -58,7 +58,7 @@ let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }=
 let vernac_decl_proof () = 
   let pf = Proof_global.give_me_the_proof () in
   if Proof.is_done pf then 
-    Errors.error "Nothing left to prove here."
+    CErrors.error "Nothing left to prove here."
   else
     begin
       Decl_proof_instr.go_to_proof_mode () ;
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index 4c71f04107..59a0bb5a2d 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Pp
 open Decl_expr
 open Names
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 5d1551106f..e39d17b52d 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -51,9 +51,9 @@ let start_deriving f suchthat lemma =
           [suchthat], respectively. *)
       let (opaque,f_def,lemma_def) =
         match com with
-        | Admitted _ -> Errors.error"Admitted isn't supported in Derive."
+        | Admitted _ -> CErrors.error"Admitted isn't supported in Derive."
         | Proved (_,Some _,_) ->
-            Errors.error"Cannot save a proof of Derive with an explicit name."
+            CErrors.error"Cannot save a proof of Derive with an explicit name."
         | Proved (opaque, None, obj) ->
             match Proof_global.(obj.entries) with
             | [_;f_def;lemma_def] ->
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
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 2ed436c6bf..58744b5754 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -19,7 +19,7 @@ open Context.Rel.Declaration
 
 let qflag=ref true
 
-let red_flags=ref Closure.betaiotazeta
+let red_flags=ref CClosure.betaiotazeta
 
 let (=?) f g i1 i2 j1 j2=
   let c=f i1 i2 in
@@ -59,12 +59,12 @@ let ind_hyps nevar ind largs gls=
     Array.map myhyps types
 
 let special_nf gl=
-  let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
-    (fun t -> Closure.norm_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in
+    (fun t -> CClosure.norm_val infos (CClosure.inject t))
 
 let special_whd gl=
-  let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in
+    (fun t -> CClosure.whd_val infos (CClosure.inject t))
 
 type kind_of_formula=
     Arrow of constr*constr
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 0f70d3ea05..5db8ff59ad 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -11,7 +11,7 @@ open Globnames
 
 val qflag : bool ref
 
-val red_flags: Closure.RedFlags.reds ref
+val red_flags: CClosure.RedFlags.reds ref
 
 val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) ->
   'a -> 'a -> 'b -> 'b -> int
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index d7da85b4f4..628af4e719 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -24,8 +24,8 @@ let update_flags ()=
   in
     List.iter f (Classops.coercions ());
     red_flags:=
-    Closure.RedFlags.red_add_transparent
-      Closure.betaiotazeta
+    CClosure.RedFlags.red_add_transparent
+      CClosure.betaiotazeta
       (Names.Id.Pred.full,Names.Cpred.complement !predref)
 
 let ground_tac solver startseq gl=
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 1394f47649..eebd974ea8 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -8,7 +8,7 @@
 
 open Unify
 open Rules
-open Errors
+open CErrors
 open Util
 open Term
 open Vars
@@ -156,7 +156,7 @@ let left_instance_tac (inst,id) continue seq=
 		      (mkApp(idc,[|ot|])) rc in
 		  let evmap, _ =
 		    try Typing.type_of (pf_env gl) evmap gt
-		    with e when Errors.noncritical e ->
+		    with e when CErrors.noncritical e ->
 		      error "Untypable instance, maybe higher-order non-prenex quantification" in
 		    tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
 	    else
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 92b6e828e8..ffb63af072 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Term
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 3e8033da07..1248b60a76 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Term
-open Errors
+open CErrors
 open Util
 open Formula
 open Unify
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index dc5dd45ab0..51bd3009ae 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -501,11 +501,11 @@ let rec fourier () =
 		        with NoIneq -> ())
               hyps;
     (* lineq = les inéquations découlant des hypothèses *)
-    if !lineq=[] then Errors.error "No inequalities";
+    if !lineq=[] then CErrors.error "No inequalities";
     let res=fourier_lineq (!lineq) in
     let tac=ref (Proofview.tclUNIT ()) in
     if res=[]
-    then Errors.error "fourier failed"
+    then CErrors.error "fourier failed"
     (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
     else (match res with
         [(cres,sres,lc)]->
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 146749d32b..b0ffc775b5 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,5 +1,5 @@
 open Printer
-open Errors
+open CErrors
 open Util
 open Term
 open Vars
@@ -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 );
@@ -52,7 +52,7 @@ let rec print_debug_queue e =
       let _ =
 	match e with
 	| Some e ->
-	   Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
+	   Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal))
 	| None ->
 	   begin
 	     Feedback.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal);
@@ -74,9 +74,9 @@ let do_observe_tac s tac g =
     ignore(Stack.pop debug_queue);
     v
   with reraise ->
-    let reraise = Errors.push reraise in
+    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 =
@@ -141,7 +141,7 @@ let is_trivial_eq t =
 	    eq_constr t1 t2 && eq_constr a1 a2
 	| _ -> false
     end
-  with e when Errors.noncritical e -> false
+  with e when CErrors.noncritical e -> false
   in
 (*   observe (str "is_trivial_eq " ++ Printer.pr_lconstr t ++ (if res then str " true" else str " false")); *)
   res
@@ -167,7 +167,7 @@ let is_incompatible_eq t =
 	    (eq_constr u1 u2 &&
 	       incompatible_constructor_terms t1 t2)
 	| _ -> false
-    with e when Errors.noncritical e -> false
+    with e when CErrors.noncritical e -> false
   in
   if res then   observe (str "is_incompatible_eq " ++ Printer.pr_lconstr t);
   res
@@ -223,8 +223,8 @@ let isAppConstruct ?(env=Global.env ()) t =
 
 let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta  *)
   let clos_norm_flags flgs env sigma t =
-    Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
-  clos_norm_flags Closure.betaiotazeta  Environ.empty_env Evd.empty
+    CClosure.norm_val (CClosure.create_clos_infos flgs env) (CClosure.inject (Reductionops.nf_evar sigma t)) in
+  clos_norm_flags CClosure.betaiotazeta  Environ.empty_env Evd.empty
 
 
 
@@ -254,7 +254,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
 	  then
 	    (jmeq_refl (),(args.(1),args.(0)),(args.(3),args.(2)),args.(0))
 	  else nochange "not an equality"
-      with e when Errors.noncritical e -> nochange "not an equality"
+      with e when CErrors.noncritical e -> nochange "not an equality"
     in
     if not ((closed0 (fst t1)) && (closed0 (snd t1)))then nochange "not a closed lhs";
     let rec compute_substitution sub t1 t2 =
@@ -625,8 +625,8 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 let my_orelse tac1 tac2 g =
   try
     tac1 g
-  with e when Errors.noncritical e ->
-(*     observe (str "using snd tac since : " ++ Errors.print e); *)
+  with e when CErrors.noncritical e ->
+(*     observe (str "using snd tac since : " ++ CErrors.print e); *)
     tac2 g
 
 let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
@@ -1025,7 +1025,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
 		{finfos with
 		   equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
 					      ConstRef c -> c
-					    | _ -> Errors.anomaly (Pp.str "Not a constant")
+					    | _ -> CErrors.anomaly (Pp.str "Not a constant")
 					 )
 		}
 	  | _ -> ()
@@ -1085,7 +1085,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
       match Global.body_of_constant const with
 	| Some body ->
 	     Tacred.cbv_norm_flags
-	       (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+	       (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 	       (Global.env ())
 	       (Evd.empty)
 	       body
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 5b4fb25955..5e72b8672a 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,5 +1,5 @@
 open Printer
-open Errors
+open CErrors
 open Util
 open Term
 open Vars
@@ -358,7 +358,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
      Don't forget to close the goal if an error is raised !!!!
   *)
   save false new_princ_name entry g_kind hook
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
     begin
       begin
 	try
@@ -370,7 +370,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
 	  then Pfedit.delete_current_proof ()
 	  else ()
 	  else ()
-	with e when Errors.noncritical e -> ()
+	with e when CErrors.noncritical e -> ()
       end;
       raise (Defining_principle e)
     end
@@ -400,7 +400,7 @@ let get_funs_constant mp dp =
       match Global.body_of_constant const with
 	| Some body ->
 	    let body = Tacred.cbv_norm_flags
-	      (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+	      (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 	      (Global.env ())
 	      (Evd.from_env (Global.env ()))
 	      body
@@ -510,7 +510,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
 	0
 	(prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs)))
 	(fun _ _ _ -> ())
-    with e when Errors.noncritical e ->
+    with e when CErrors.noncritical e ->
        begin
 	 begin
 	   try
@@ -522,7 +522,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
 		  then Pfedit.delete_current_proof ()
 		  else ()
 	     else ()
-	   with e when Errors.noncritical e -> ()
+	   with e when CErrors.noncritical e -> ()
 	 end;
 	 raise (Defining_principle e)
        end
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 93a89330e3..42e4903155 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -90,7 +90,7 @@ let pr_intro_as_pat _prc _ _ pat =
 
 let out_disjunctive = function
   | loc, IntroAction (IntroOrAndPattern l) -> (loc,l)
-  | _ -> Errors.error "Disjunctive or conjunctive intro pattern expected."
+  | _ -> CErrors.error "Disjunctive or conjunctive intro pattern expected."
 
 ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat
 |   [ "as"  simple_intropattern(ipat) ] -> [ Some ipat ]
@@ -195,15 +195,15 @@ 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
-       let error = if do_observe () then (spc () ++ Errors.print e) else mt () in
+       let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in
        warn_cannot_define_graph (names,error)
     | Defining_principle e ->
        let names = pr_enum Libnames.pr_reference names in
-       let error = if do_observe () then Errors.print e else mt () in
+       let error = if do_observe () then CErrors.print e else mt () in
        warn_cannot_define_principle (names,error)
     | _ -> raise e
 
@@ -227,15 +227,15 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
 		  ;
 		    try Functional_principles_types.build_scheme fas
 		    with Functional_principles_types.No_graph_found ->
-		      Errors.error ("Cannot generate induction principle(s)")
-		      | e when Errors.noncritical e ->
+		      CErrors.error ("Cannot generate induction principle(s)")
+		      | e when CErrors.noncritical e ->
 			  let names = List.map (fun (_,na,_) -> na) fas in
 			  warning_error names e
 
 		  end
 	      | _ -> assert false (* we can only have non empty  list *)
 	  end
-	  | e when Errors.noncritical e ->
+	  | e when CErrors.noncritical e ->
 	      let names = List.map (fun (_,na,_) -> na) fas in
 	      warning_error names e
       end
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index c424fe1226..52179ae508 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -7,7 +7,7 @@ open Glob_term
 open Glob_ops
 open Globnames
 open Indfun_common
-open Errors
+open CErrors
 open Util
 open Glob_termops
 open Misctypes
@@ -921,7 +921,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    observe (str "computing new type for eq : " ++ pr_glob_constr rt);
 		    let t' =
 		      try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*)
-                      with e when Errors.noncritical e -> raise Continue
+                      with e when CErrors.noncritical e -> raise Continue
 		    in
 		    let is_in_b = is_free_in id b in
 		    let _keep_eq =
@@ -1223,7 +1223,7 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool)
 	     l := param::!l
 	)
 	rels_params.(0)
-    with e when Errors.noncritical e ->
+    with e when CErrors.noncritical e ->
       ()
   in
   List.rev !l
@@ -1460,7 +1460,7 @@ let do_build_inductive
 	  str "while trying to define"++ spc () ++
 	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds))
 	    ++ fnl () ++
-	    Errors.print reraise
+	    CErrors.print reraise
 	in
  	observe msg;
 	raise reraise
@@ -1476,7 +1476,7 @@ let build_inductive evd funconstants funsargs returned_types rtl =
     do_build_inductive evd funconstants funsargs returned_types rtl;
     Detyping.print_universes := pu;
     Constrextern.print_universes := cu
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
     Detyping.print_universes := pu;
     Constrextern.print_universes := cu;
     raise (Building_graph e)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 291f835ee7..01e5ef7fba 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -1,6 +1,6 @@
 open Pp
 open Glob_term
-open Errors
+open CErrors
 open Util
 open Names
 open Decl_kinds
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2ebbb34e4c..18817f504c 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,5 +1,5 @@
 open Context.Rel.Declaration
-open Errors
+open CErrors
 open Util
 open Names
 open Term
@@ -225,12 +225,12 @@ 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"
     (fun e' -> strbrk "Cannot build inversion information" ++
-                 if do_observe () then (fnl() ++ Errors.print e') else mt ())
+                 if do_observe () then (fnl() ++ CErrors.print e') else mt ())
 
 let derive_inversion fix_names =
   try
@@ -272,10 +272,10 @@ let derive_inversion fix_names =
 	functional_induction
 	fix_names_as_constant
 	lind;
-      with e when Errors.noncritical e ->
+      with e when CErrors.noncritical e ->
       let e' = process_vernac_interp_error e in
       warn_funind_cannot_build_inversion e'
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
     let e' = process_vernac_interp_error e in
     warn_funind_cannot_build_inversion e'
 
@@ -295,12 +295,12 @@ let warning_error names e =
     match e with
       | ToShow e -> 
 	let e = process_vernac_interp_error e in
-	spc () ++ Errors.print e
+	spc () ++ CErrors.print e
       | _ -> 
 	if do_observe () 
 	then 
 	  let e = process_vernac_interp_error e in 
-	  (spc () ++ Errors.print e) 
+	  (spc () ++ CErrors.print e)
 	else mt ()
   in
   match e with
@@ -316,8 +316,8 @@ let error_error names e =
   let e = process_vernac_interp_error e in
   let e_explain e =
     match e with
-      | ToShow e -> spc () ++ Errors.print e
-      | _ -> if do_observe () then (spc () ++ Errors.print e) else mt ()
+      | ToShow e -> spc () ++ CErrors.print e
+      | _ -> if do_observe () then (spc () ++ CErrors.print e) else mt ()
   in
   match e with
     | Building_graph e ->
@@ -385,7 +385,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	Array.iter (add_Function is_general) funs_kn;
 	()
       end
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
     on_error names e
 
 let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
@@ -475,7 +475,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	   functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
 	);
       derive_inversion [fname]
-    with e when Errors.noncritical e ->
+    with e when CErrors.noncritical e ->
       (* No proof done *)
       ()
   in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 2449678a13..f56e92414e 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -49,7 +49,7 @@ let locate_constant ref =
 
 let locate_with_msg msg f x =
   try f x
-  with Not_found -> raise (Errors.UserError("", msg))
+  with Not_found -> raise (CErrors.UserError("", msg))
 
 
 let filter_map filter f =
@@ -73,7 +73,7 @@ let chop_rlambda_n  =
 	  | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
 	  | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
 	  | _ ->
-	      raise (Errors.UserError("chop_rlambda_n",
+	      raise (CErrors.UserError("chop_rlambda_n",
 				    str "chop_rlambda_n: Not enough Lambdas"))
   in
   chop_lambda_n []
@@ -85,7 +85,7 @@ let chop_rprod_n  =
       else
 	match rt with
 	  | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
-	  | _ -> raise (Errors.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products"))
+	  | _ -> raise (CErrors.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products"))
   in
   chop_prod_n []
 
@@ -110,7 +110,7 @@ let const_of_id id =
   in
   try Constrintern.locate_reference princ_ref
   with Not_found ->
-    Errors.errorlabstrm "IndFun.const_of_id"
+    CErrors.errorlabstrm "IndFun.const_of_id"
       (str "cannot find " ++ Nameops.pr_id id)
 
 let def_of_const t =
@@ -344,7 +344,7 @@ let pr_info f_info =
   (try
      Printer.pr_lconstr
        (Global.type_of_global_unsafe (ConstRef f_info.function_constant))
-   with e when Errors.noncritical e -> mt ()) ++ fnl () ++
+   with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
   str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
   str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
   str "correctness_lemma := " ++ pr_ocst f_info.correctness_lemma ++ fnl () ++
@@ -371,7 +371,7 @@ let in_Function : function_info -> Libobject.obj =
 
 let find_or_none id =
   try Some
-    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly (Pp.str "Not a constant")
+    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant")
     )
   with Not_found -> None
 
@@ -399,7 +399,7 @@ let add_Function is_general f =
   and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
   and graph_ind =
     match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
-    with | IndRef ind -> ind | _ -> Errors.anomaly (Pp.str "Not an inductive")
+    with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive")
   in
   let finfos =
     { function_constant = f;
@@ -476,13 +476,13 @@ let jmeq () =
   try
     Coqlib.check_required_library Coqlib.jmeq_module_name;
     Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq"
-  with e when Errors.noncritical e -> raise (ToShow e)
+  with e when CErrors.noncritical e -> raise (ToShow e)
 
 let jmeq_refl () =
   try
     Coqlib.check_required_library Coqlib.jmeq_module_name;
     Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq_refl"
-  with e when Errors.noncritical e -> raise (ToShow e)
+  with e when CErrors.noncritical e -> raise (ToShow e)
 
 let h_intros l =
   tclMAP (fun x -> Proofview.V82.of_tactic (Tactics.Simple.intro x)) l
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 1ff254f6ca..26fc88a604 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -8,7 +8,7 @@
 
 open Tacexpr
 open Declarations
-open Errors
+open CErrors
 open Util
 open Names
 open Term
@@ -65,16 +65,16 @@ let observe strm =
 let do_observe_tac s tac g =
   let goal =
     try Printer.pr_goal g
-    with e when Errors.noncritical e -> assert false
+    with e when CErrors.noncritical e -> assert false
   in
   try
     let v = tac g in
     msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
   with reraise ->
-    let reraise = Errors.push reraise in
-    let e = Cerrors.process_vernac_interp_error reraise in
+    let reraise = CErrors.push reraise in
+    let e = ExplainErr.process_vernac_interp_error reraise in
     observe (hov 0 (str "observation "++ s++str " raised exception " ++
-	     Errors.iprint e ++ str " on goal" ++ fnl() ++ goal ));
+	     CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal ));
     iraise reraise;;
 
 
@@ -90,7 +90,7 @@ let observe_tac s tac g =
 
 (* [nf_zeta] $\zeta$-normalization of a term *)
 let nf_zeta =
-  Reductionops.clos_norm_flags  (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+  Reductionops.clos_norm_flags  (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
     Environ.empty_env
     Evd.empty
 
@@ -585,7 +585,7 @@ let rec reflexivity_with_destruct_cases g =
 	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
 	    ]
         | _ -> Proofview.V82.of_tactic reflexivity
-    with e when Errors.noncritical e -> Proofview.V82.of_tactic reflexivity
+    with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity
   in
   let eq_ind = make_eq () in
   let discr_inject =
@@ -998,7 +998,7 @@ let invfun qhyp f  =
   let f =
     match f with
       | ConstRef f -> f
-      | _ -> raise (Errors.UserError("",str "Not a function"))
+      | _ -> raise (CErrors.UserError("",str "Not a function"))
   in
   try
     let finfos = find_Function_infos f in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 99a165044c..de4210af5f 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -11,7 +11,7 @@
 open Globnames
 open Tactics
 open Indfun_common
-open Errors
+open CErrors
 open Util
 open Constrexpr
 open Vernacexpr
@@ -73,7 +73,7 @@ let ident_global_exist id =
     let ans = CRef (Libnames.Ident (Loc.ghost,id), None) in
     let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in
     true
-  with e when Errors.noncritical e -> false
+  with e when CErrors.noncritical e -> false
 
 (** [next_ident_fresh id] returns a fresh identifier (ie not linked in
     global env) with base [id]. *)
@@ -785,10 +785,10 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
 
   let params1 =
     try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1))
-    with e when Errors.noncritical e -> [] in
+    with e when CErrors.noncritical e -> [] in
   let params2 =
     try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2))
-    with e when Errors.noncritical e -> [] in
+    with e when CErrors.noncritical e -> [] in
 
   let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in
   let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ceea4fa535..62f3071151 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -16,7 +16,7 @@ open Names
 open Libnames
 open Globnames
 open Nameops
-open Errors
+open CErrors
 open Util
 open Tacticals
 open Tacmach
@@ -92,15 +92,15 @@ let const_of_ref = function
 
 
 let nf_zeta env =
-  Reductionops.clos_norm_flags  (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+  Reductionops.clos_norm_flags  (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
     env
     Evd.empty
 
 
 let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta  *)
   let clos_norm_flags flgs env sigma t =
-    Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
-  clos_norm_flags Closure.betaiotazeta  Environ.empty_env Evd.empty
+    CClosure.norm_val (CClosure.create_clos_infos flgs env) (CClosure.inject (Reductionops.nf_evar sigma t)) in
+  clos_norm_flags CClosure.betaiotazeta  Environ.empty_env Evd.empty
 
 
 
@@ -214,7 +214,7 @@ let print_debug_queue b e =
     begin
       let lmsg,goal = Stack.pop debug_queue in 
       if b then 
-	Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal))
+	Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal))
       else
 	begin
 	  Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
@@ -238,9 +238,9 @@ let do_observe_tac s tac g =
     ignore(Stack.pop debug_queue);
     v
   with reraise ->
-    let reraise = Errors.push reraise in
+    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 =
@@ -441,7 +441,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	try
 	  check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info
-	with e when Errors.noncritical e ->
+	with e when CErrors.noncritical e ->
 	  errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
       end
     | Lambda(n,t,b) -> 
@@ -449,7 +449,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	try
 	  check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info
-	with e when Errors.noncritical e ->
+	with e when CErrors.noncritical e ->
 	  errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
       end
     | Case(ci,t,a,l) -> 
@@ -645,7 +645,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
       try 
 	check_not_nested (expr_info.f_id::expr_info.forbidden_ids) b;
 	true
-      with e when Errors.noncritical e -> false
+      with e when CErrors.noncritical e -> false
     in
     if forbid 
     then 
@@ -704,7 +704,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
     try
       check_not_nested (expr_info.f_id::expr_info.forbidden_ids) a;
       false
-    with e when Errors.noncritical e ->
+    with e when CErrors.noncritical e ->
       true
   in
   let a' = infos.info in
@@ -1281,12 +1281,12 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
     | Some s -> s
     | None   ->
 	try add_suffix current_proof_name "_subproof"
-	with e when Errors.noncritical e ->
+	with e when CErrors.noncritical e ->
           anomaly (Pp.str "open_new_goal with an unamed theorem")
   in
   let na = next_global_ident_away name [] in
   if Termops.occur_existential gls_type then
-    Errors.error "\"abstract\" cannot handle existentials";
+    CErrors.error "\"abstract\" cannot handle existentials";
   let hook _ _ =
     let opacity =
       let na_ref = Libnames.Ident (Loc.ghost,na) in
@@ -1534,10 +1534,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
     let stop = 
       try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
 	  false
-      with e when Errors.noncritical e ->
+      with e when CErrors.noncritical e ->
 	begin
 	  if do_observe ()
-	  then Feedback.msg_debug (str "Cannot create equation Lemma " ++ Errors.print e)
+	  then Feedback.msg_debug (str "Cannot create equation Lemma " ++ CErrors.print e)
 	  else anomaly (Pp.str "Cannot create equation Lemma")
 	  ;
 	  true
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 1561c811cd..459c72f9f6 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -331,7 +331,7 @@ let dual_raw_certificate (l:  (Poly.t * Mc.op1) list) =
   | Inr _ -> None
   | Inl cert ->  Some (rats_to_ints (Vect.to_list cert)) 
   (* should not use rats_to_ints *)
- with x when Errors.noncritical x ->
+ with x when CErrors.noncritical x ->
   if debug
   then (Printf.printf "raw certificate %s" (Printexc.to_string x);
         flush stdout) ;
@@ -378,7 +378,7 @@ let linear_prover n_spec l  =
 
 let linear_prover n_spec l  =
  try linear_prover n_spec l
- with x when Errors.noncritical x ->
+ with x when CErrors.noncritical x ->
   (print_string (Printexc.to_string x); None)
 
 let compute_max_nb_cstr l d =
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index e4aa1448eb..b8e5e66cab 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -998,7 +998,7 @@ struct
                            let (expr,env) = parse_expr env args.(0) in
                            let power = (parse_exp expr args.(1)) in
                              (power  , env)
-			 with e when Errors.noncritical e ->
+			 with e when CErrors.noncritical e ->
                            (* if the exponent is a variable *)
                            let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env)
                        end
@@ -1170,7 +1170,7 @@ struct
       try
         let (at,env) = parse_atom env t gl in
         (A(at,tg,t), env,Tag.next tg)
-      with e when Errors.noncritical e -> (X(t),env,tg) in
+      with e when CErrors.noncritical e -> (X(t),env,tg) in
 
     let is_prop term =
      let ty   = Typing.unsafe_type_of (Tacmach.pf_env gl) (Tacmach.project gl) term in
@@ -1318,7 +1318,7 @@ let btree_of_array typ a  =
 let btree_of_array typ a =
  try
   btree_of_array typ a
- with x when Errors.noncritical x ->
+ with x when CErrors.noncritical x ->
   failwith (Printf.sprintf "btree of array : %s" (Printexc.to_string x))
 
 let dump_varmap typ env =
@@ -1387,7 +1387,7 @@ let rec parse_hyps gl parse_arith env tg hyps =
       try
        let (c,env,tg) = parse_formula gl parse_arith env  tg t in
 	((i,c)::lhyps, env,tg)
-      with e when Errors.noncritical e -> (lhyps,env,tg)
+      with e when CErrors.noncritical e -> (lhyps,env,tg)
        (*(if debug then Printf.printf "parse_arith : %s\n" x);*)
 
 
@@ -1547,7 +1547,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
           (pp_ml_list prover.pp_f) (List.map fst new_cl)   ;
           flush stdout
       end ; *)
-    let res = try prover.compact prf remap with x when Errors.noncritical x ->
+    let res = try prover.compact prf remap with x when CErrors.noncritical x ->
       if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ;
       (* This should not happen -- this is the recovery plan... *)
       match prover.prover (prover.get_option () ,List.map fst new_cl) with
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index e22fe58434..f4f9b3c2f1 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -734,7 +734,7 @@ struct
 	| Inl (s,_) ->
 	    try
 	      Some (bound_of_variable IMap.empty fresh s.sys)
-	    with x when Errors.noncritical x ->
+	    with x when CErrors.noncritical x ->
 	      Printf.printf "optimise Exception : %s" (Printexc.to_string x);
               None
 
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 88b13abf9a..0e6d346a3b 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -92,7 +92,7 @@ let read_key_elem inch =
     Some (Marshal.from_channel inch)
   with
     | End_of_file -> None
-    | e when Errors.noncritical e -> raise InvalidTableFormat
+    | e when CErrors.noncritical e -> raise InvalidTableFormat
 
 (** 
     We used to only lock/unlock regions.
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index ee1904a660..93dad18d98 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Term
 open Tactics
diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml
index 8e2fc07c04..922432460d 100644
--- a/plugins/nsatz/utile.ml
+++ b/plugins/nsatz/utile.ml
@@ -51,7 +51,7 @@ let facteurs_liste div constant lp =
                                    if not (constant r)
 				   then l1:=r::(!l1)
                                    else p_dans_lmin:=true)
-			      with e when Errors.noncritical e -> ())
+			      with e when CErrors.noncritical e -> ())
                      lmin;
           if !p_dans_lmin
           then factor lmin lp1
@@ -62,7 +62,7 @@ let facteurs_liste div constant lp =
                 List.iter (fun q -> try (let r = div q p in
 					 if not (constant r)
 					 then l1:=r::(!l1))
-				    with e when Errors.noncritical e ->
+				    with e when CErrors.noncritical e ->
                                       lmin1:=q::(!lmin1))
                           lmin;
 	        factor (List.rev (p::(!lmin1))) !l1)
@@ -93,7 +93,7 @@ let factorise_tableau div zero c f l1 =
       	                       li:=j::(!li);
                                r:=rr;
 			   done)
-                      with e when Errors.noncritical e -> ())
+                      with e when CErrors.noncritical e -> ())
                   l1;
       res.(i)<-(!r,!li))
      f;
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 0bf30e7fd8..d625e3076a 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -13,7 +13,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops
@@ -911,7 +911,7 @@ let rec transform p t =
     try
       let v,th,_ = find_constr t' in
       [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
-    with e when Errors.noncritical e ->
+    with e when CErrors.noncritical e ->
       let v = new_identifier_var ()
       and th = new_identifier () in
       hide_constr t' v th isnat;
@@ -951,7 +951,7 @@ let rec transform p t =
        end
    | Kapp((Zpos|Zneg|Z0),_) ->
        (try ([],Oz(recognize_number t))
-        with e when Errors.noncritical e -> default false t)
+        with e when CErrors.noncritical e -> default false t)
    | Kvar s -> [],Oatom s
    | Kapp(Zopp,[t]) ->
        let tac,t' = transform (P_APP 1 :: p) t in
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index d7538146f9..5647fbf9fc 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -34,7 +34,7 @@ let omega_tactic l =
        | "positive" -> eval_tactic "zify_positive"
        | "N" -> eval_tactic "zify_N"
        | "Z" -> eval_tactic "zify_op"
-       | s -> Errors.error ("No Omega knowledge base for type "^s))
+       | s -> CErrors.error ("No Omega knowledge base for type "^s))
     (Util.List.sort_uniquize String.compare l)
   in
   Tacticals.New.tclTHEN
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index dbd7460e25..b3ea4335f6 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -101,7 +101,7 @@
 
 
 (*i*)
-open Errors
+open CErrors
 open Util
 open Names
 open Term
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 21b0f78b5a..4935fe4bbc 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -39,7 +39,7 @@ let destructurate t =
     | Term.Var id,[] -> Kvar(Names.Id.to_string id)
     | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
     | Term.Prod (Names.Name _,_,_),[] ->
-	Errors.error "Omega: Not a quantifier-free goal"
+	CErrors.error "Omega: Not a quantifier-free goal"
     | _ -> Kufo
 
 exception Destruct
@@ -346,7 +346,7 @@ let parse_term t =
     | Kapp("Z.succ",[t]) -> Tsucc t
     | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one))
     | Kapp(("Zpos"|"Zneg"|"Z0"),_) ->
-	(try Tnum (recognize t) with e when Errors.noncritical e -> Tother)
+	(try Tnum (recognize t) with e when CErrors.noncritical e -> Tother)
     | _ -> Tother
   with e when Logic.catchable_exception e -> Tother
 
@@ -368,6 +368,6 @@ let is_scalar t =
     | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> aux t
     | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true
     | _ -> false in
-  try aux t with e when Errors.noncritical e -> false
+  try aux t with e when CErrors.noncritical e -> false
 
 end
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index fd4ede6c3d..830dc54ddb 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -27,7 +27,7 @@ let romega_tactic l =
        | "positive" -> eval_tactic "zify_positive"
        | "N" -> eval_tactic "zify_N"
        | "Z" -> eval_tactic "zify_op"
-       | s -> Errors.error ("No ROmega knowledge base for type "^s))
+       | s -> CErrors.error ("No ROmega knowledge base for type "^s))
     (Util.List.sort_uniquize String.compare l)
   in
   Tacticals.New.tclTHEN
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index a059512d84..ba882e39a2 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -454,7 +454,7 @@ let rec scalar n = function
  | Omult(t1,Oint x) ->
      do_list [Lazy.force coq_c_mult_assoc_reduced], Omult(t1,Oint (n*x))
  | Omult(t1,t2) ->
-     Errors.error "Omega: Can't solve a goal with non-linear products"
+     CErrors.error "Omega: Can't solve a goal with non-linear products"
  | (Oatom _ as t) -> do_list [], Omult(t,Oint n)
  | Oint i -> do_list [Lazy.force coq_c_reduce],Oint(n*i)
  | (Oufo _ as t)-> do_list [], Oufo (Omult(t,Oint n))
@@ -473,7 +473,7 @@ let rec negate = function
  | Omult(t1,Oint x) ->
      do_list [Lazy.force coq_c_opp_mult_r], Omult(t1,Oint (Bigint.neg x))
  | Omult(t1,t2) ->
-     Errors.error "Omega: Can't solve a goal with non-linear products"
+     CErrors.error "Omega: Can't solve a goal with non-linear products"
  | (Oatom _ as t) ->
      do_list [Lazy.force coq_c_opp_one], Omult(t,Oint(negone))
  | Oint i -> do_list [Lazy.force coq_c_reduce] ,Oint(Bigint.neg i)
@@ -545,7 +545,7 @@ let shrink_pair f1 f2 =
        Lazy.force coq_c_red4, Omult(Oatom v,Oplus(c1,c2))
    | t1,t2 ->
        oprint stdout t1; print_newline (); oprint stdout t2; print_newline ();
-       flush Pervasives.stdout; Errors.error "shrink.1"
+       flush Pervasives.stdout; CErrors.error "shrink.1"
   end
 
 (* \subsection{Calcul d'une sous formule constante} *)
@@ -559,9 +559,9 @@ let reduce_factor = function
       let rec compute = function
           Oint n -> n
 	| Oplus(t1,t2) -> compute t1 + compute t2
-	| _ -> Errors.error "condense.1" in
+	| _ -> CErrors.error "condense.1" in
 	[Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c))
-  | t -> Errors.error "reduce_factor.1"
+  | t -> CErrors.error "reduce_factor.1"
 
 (* \subsection{Réordonnancement} *)
 
@@ -1304,7 +1304,7 @@ let total_reflexive_omega_tactic gl =
   let systems_list = destructurate_hyps full_reified_goal in
   if !debug then display_systems systems_list;
   resolution env full_reified_goal systems_list gl
-  with NO_CONTRADICTION -> Errors.error "ROmega can't solve this system"
+  with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system"
 
 
 (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*)
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index f3eae5f501..8b92611136 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Goptions
 
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index bb9266db1d..4ed9079517 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -8,7 +8,7 @@
 
 module Search = Explore.Make(Proof_search)
 
-open Errors
+open CErrors
 open Util
 open Term
 open Tacmach
@@ -67,12 +67,12 @@ let l_D_Or = lazy (constant "D_Or")
 
 
 let special_whd gl=
-  let infos=Closure.create_clos_infos Closure.all (pf_env gl) in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in
+    (fun t -> CClosure.whd_val infos (CClosure.inject t))
 
 let special_nf gl=
-  let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in
-    (fun t -> Closure.norm_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in
+    (fun t -> CClosure.norm_val infos (CClosure.inject t))
 
 type atom_env=
     {mutable next:int;
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index a6744916ae..90f5f8e63d 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -7,12 +7,12 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Term
 open Vars
-open Closure
+open CClosure
 open Environ
 open Libnames
 open Globnames
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 814e3a4d5a..ff1db8cf53 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -61,8 +61,8 @@ DECLARE PLUGIN "ssrmatching_plugin"
 
 type loc = Loc.t
 let dummy_loc = Loc.ghost
-let errorstrm = Errors.errorlabstrm "ssrmatching"
-let loc_error loc msg = Errors.user_err_loc (loc, msg, str msg)
+let errorstrm = CErrors.errorlabstrm "ssrmatching"
+let loc_error loc msg = CErrors.user_err_loc (loc, msg, str msg)
 let ppnl = Feedback.msg_info
 
 (* 0 cost pp function. Active only if env variable SSRDEBUG is set *)
@@ -89,7 +89,7 @@ let env_size env = List.length (Environ.named_context env)
 let safeDestApp c =
   match kind_of_term c with App (f, a) -> f, a | _ -> c, [| |]
 let get_index = function ArgArg i -> i | _ ->
-  Errors.anomaly (str"Uninterpreted index")
+  CErrors.anomaly (str"Uninterpreted index")
 (* Toplevel constr must be globalized twice ! *)
 let glob_constr ist genv = function
   | _, Some ce ->
@@ -150,7 +150,7 @@ let dC t = CastConv t
 (** Constructors for constr_expr *)
 let isCVar = function CRef (Ident _, _) -> true | _ -> false
 let destCVar = function CRef (Ident (_, id), _) -> id | _ ->
-  Errors.anomaly (str"not a CRef")
+  CErrors.anomaly (str"not a CRef")
 let mkCHole loc = CHole (loc, None, IntroAnonymous, None)
 let mkCLambda loc name ty t = 
    CLambdaN (loc, [[loc, name], Default Explicit, ty], t)
@@ -167,8 +167,8 @@ let mkRLambda n s t = GLambda (dummy_loc, n, Explicit, s, t)
 let combineCG t1 t2 f g = match t1, t2 with
  | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None)
  | (x, (_, Some t1)), (_, (_, Some t2)) -> x, (mkRHole, Some (f t1 t2))
- | _, (_, (_, None)) -> Errors.anomaly (str"have: mixed C-G constr")
- | _ -> Errors.anomaly (str"have: mixed G-C constr")
+ | _, (_, (_, None)) -> CErrors.anomaly (str"have: mixed C-G constr")
+ | _ -> CErrors.anomaly (str"have: mixed G-C constr")
 let loc_ofCG = function
  | (_, (s, None)) -> Glob_ops.loc_of_glob_constr s
  | (_, (_, Some s)) -> Constrexpr_ops.constr_loc s
@@ -491,7 +491,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p =
     | Evar (k, _) ->
       if Evd.mem sigma0 k then KpatEvar k, f, a else
       if a <> [] then KpatFlex, f, a else 
-      (match p_origin with None -> Errors.error "indeterminate pattern"
+      (match p_origin with None -> CErrors.error "indeterminate pattern"
       | Some (dir, rule) ->
 	errorstrm (str "indeterminate " ++ pr_dir_side dir
           ++ str " in " ++ pr_constr_pat rule))
@@ -632,12 +632,12 @@ let match_upats_FO upats env sigma0 ise orig_c =
            let pt' = unif_end env sigma0 ise' u.up_t (u.up_ok lhs) in
            raise (FoundUnif (ungen_upat lhs pt' u))
        with FoundUnif (s,_,_) as sig_u when dont_impact_evars s -> raise sig_u
-       | Not_found -> Errors.anomaly (str"incomplete ise in match_upats_FO")
+       | Not_found -> CErrors.anomaly (str"incomplete ise in match_upats_FO")
        | _ -> () in
     List.iter one_match fpats
   done;
   iter_constr_LR loop f; Array.iter loop a in
-  try loop orig_c with Invalid_argument _ -> Errors.anomaly (str"IN FO")
+  try loop orig_c with Invalid_argument _ -> CErrors.anomaly (str"IN FO")
 
 let prof_FO = mk_profiler "match_upats_FO";;
 let match_upats_FO upats env sigma0 ise c =
@@ -684,7 +684,7 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
       | Pretype_errors.PretypeError
          (_,_,Pretype_errors.UnsatisfiableConstraints _) ->
           failed_because_of_TC:=true
-      | e when Errors.noncritical e -> () in
+      | e when CErrors.noncritical e -> () in
     List.iter one_match fpats
   done;
   iter_constr_LR (aux upats env sigma0 ise) f;
@@ -707,11 +707,11 @@ let fixed_upat = function
 let do_once r f = match !r with Some _ -> () | None -> r := Some (f ())
 
 let assert_done r = 
-  match !r with Some x -> x | None -> Errors.anomaly (str"do_once never called")
+  match !r with Some x -> x | None -> CErrors.anomaly (str"do_once never called")
 
 let assert_done_multires r = 
   match !r with
-  | None -> Errors.anomaly (str"do_once never called")
+  | None -> CErrors.anomaly (str"do_once never called")
   | Some (n, xs) ->
       r := Some (n+1,xs);
       try List.nth xs n with Failure _ -> raise NoMatch
@@ -768,7 +768,7 @@ let source () = match upats_origin, upats with
   | Some (dir,rule), _ -> str"The " ++ pr_dir_side dir ++ str" of " ++ 
       pr_constr_pat rule ++ spc()
   | _, [] | None, _::_::_ ->
-      Errors.anomaly (str"mk_tpattern_matcher with no upats_origin") in
+      CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin") in
 let on_instance, instances =
   let instances = ref [] in
   (fun x ->
@@ -806,7 +806,7 @@ let rec uniquize = function
         errorstrm (source () ++ str "does not match any subterm of the goal")
     | NoProgress when (not raise_NoMatch) ->
         let dir = match upats_origin with Some (d,_) -> d | _ ->
-          Errors.anomaly (str"mk_tpattern_matcher with no upats_origin") in
+          CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin") in
         errorstrm (str"all matches of "++source()++
           str"are equal to the " ++ pr_dir_side (inv_dir dir))
     | NoProgress -> raise NoMatch);
@@ -841,7 +841,7 @@ let rec uniquize = function
   let sigma, uc, ({up_f = pf; up_a = pa} as u) =
     match !upat_that_matched with
     | Some (_,x) -> List.hd x | None when raise_NoMatch -> raise NoMatch
-    | None -> Errors.anomaly (str"companion function never called") in
+    | None -> CErrors.anomaly (str"companion function never called") in
   let p' = mkApp (pf, pa) in
   if max_occ <= !nocc then p', u.up_dir, (sigma, uc, u.up_t)
   else errorstrm (str"Only " ++ int !nocc ++ str" < " ++ int max_occ ++
@@ -1022,7 +1022,7 @@ let glob_cpattern gs p =
          | (r1, Some _), (r2, Some _) when isCVar t1 ->
              encode k "In" [r1; r2; bind_in t1 t2]
          | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2]
-         | _ -> Errors.anomaly (str"where are we?")
+         | _ -> CErrors.anomaly (str"where are we?")
          with _ when isCVar t1 -> encode k "In" [bind_in t1 t2])
      | CNotation(_, "( _ in _ in _ )", ([t1; t2; t3], [], [])) ->
          check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3]
@@ -1109,9 +1109,9 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
         let v = Id.Map.find id ist.lfun in
         Option.get reccall
           (Value.cast (topwit (Option.get wit_ssrpatternarg)) v)
-    | it -> g t with e when Errors.noncritical e -> g t in
+    | it -> g t with e when CErrors.noncritical e -> g t in
   let decodeG t f g = decode ist (mkG t) f g in
-  let bad_enc id _ = Errors.anomaly (str"bad encoding for pattern "++str id) in
+  let bad_enc id _ = CErrors.anomaly (str"bad encoding for pattern "++str id) in
   let cleanup_XinE h x rp sigma =
     let h_k = match kind_of_term h with Evar (k,_) -> k | _ -> assert false in
     let to_clean, update = (* handle rename if x is already used *)
@@ -1297,7 +1297,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
 
 let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) =
   let e = match p with
-  | In_T _ | In_X_In_T _ -> Errors.anomaly (str"pattern without redex")
+  | In_T _ | In_X_In_T _ -> CErrors.anomaly (str"pattern without redex")
   | T e | X_In_T (e, _) | E_As_X_In_T (e, _, _) | E_In_X_In_T (e, _, _) -> e in
   let sigma =
     if not resolve_typeclasses then sigma
@@ -1335,7 +1335,7 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h =
 let fill_occ_term env cl occ sigma0 (sigma, t) =
   try
     let sigma',uc,t',cl,_= pf_fill_occ env cl occ sigma0 t (sigma, t) all_ok 1 in
-    if sigma' != sigma0 then Errors.error "matching impacts evars"
+    if sigma' != sigma0 then CErrors.error "matching impacts evars"
     else cl, (Evd.merge_universe_context sigma' uc, t')
   with NoMatch -> try
     let sigma', uc, t' =
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 03b49e3336..e18d19ced4 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -11,7 +11,7 @@ let __coq_plugin_name = "ascii_syntax_plugin"
 let () = Mltop.add_known_module __coq_plugin_name
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Glob_term
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 89305838b1..a9eb126b4f 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -17,7 +17,7 @@ open Glob_term
 open Bigint
 open Coqlib
 open Pp
-open Errors
+open CErrors
 (*i*)
 
 (**********************************************************************)
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 57cb2f897a..f65f9b7910 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -100,7 +100,7 @@ let int31_of_pos_bigint dloc n =
   GApp (dloc, ref_construct, List.rev (args 31 n))
 
 let error_negative dloc =
-  Errors.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.")
+  CErrors.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.")
 
 let interp_int31 dloc n =
   if is_pos_or_zero n then
@@ -189,7 +189,7 @@ let bigN_of_pos_bigint dloc n =
   GApp (dloc, ref_constructor, args)
 
 let bigN_error_negative dloc =
-  Errors.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
+  CErrors.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
 
 let interp_bigN dloc n =
   if is_pos_or_zero n then
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index ce86c0a65f..60803a369a 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Bigint