Merge branch 'cerrors-cclosure' into trunk

Was PR#226: CErrors & CClosure

5 files changed, 13 insertions, 13 deletions

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