Merge branch 'cerrors-cclosure' into trunk

Was PR#226: CErrors & CClosure

3 files changed, 9 insertions, 9 deletions

diff --git a/dev/base_include b/dev/base_include
index 86f34b2ac9..b09b6df2de 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -66,7 +66,7 @@ open Univ
 open Inductive
 open Indtypes
 open Cooking
-open Closure
+open CClosure
 open Reduction
 open Safe_typing
 open Declare
@@ -170,7 +170,7 @@ open Tacticals
 open Tactics
 open Eqschemes
 
-open Cerrors
+open ExplainErr
 open Class
 open Command
 open Indschemes
diff --git a/dev/printers.mllib b/dev/printers.mllib
index e15855ef26..3165495488 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -37,7 +37,7 @@ Feedback
 Segmenttree
 Unicodetable
 Unicode
-Errors
+CErrors
 CWarnings
 Bigint
 CUnix
@@ -86,7 +86,7 @@ Nativecode
 Nativelib
 Cbytegen
 Environ
-Closure
+CClosure
 Reduction
 Nativeconv
 Type_errors
@@ -208,7 +208,7 @@ Dn
 Btermdn
 Hints
 Himsg
-Cerrors
+ExplainErr
 Locality
 Assumptions
 Vernacinterp
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 6074acea46..023835af76 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -80,7 +80,7 @@ let ppconstr_univ x = Constrextern.with_universes ppconstr x
 let ppglob_constr = (fun x -> pp(pr_lglob_constr x))
 let pppattern = (fun x -> pp(pr_constr_pattern x))
 let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e)))
-let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
+let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
 
 let ppbigint n = pp (str (Bigint.to_string n));;
 
@@ -457,7 +457,7 @@ let print_pure_constr csr =
 	print_string (Printexc.to_string e);print_flush ();
 	raise e
 
-let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
+let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
 
 let pploc x = let (l,r) = Loc.unloc x in
   print_string"(";print_int l;print_string",";print_int r;print_string")"
@@ -514,7 +514,7 @@ let _ =
            (fun () -> in_current_context constr_display c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
-    e -> Feedback.msg_notice (Errors.print e)
+    e -> Feedback.msg_notice (CErrors.print e)
 let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
@@ -530,7 +530,7 @@ let _ =
            (fun () -> in_current_context print_pure_constr c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
-    e -> Feedback.msg_notice (Errors.print e)
+    e -> Feedback.msg_notice (CErrors.print e)
 let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";