From f14b6f1a17652566f0cbc00ce81421ba0684dad5 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 27 Jun 2016 11:03:43 +0200 Subject: errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a --- dev/printers.mllib | 2 +- dev/top_printers.ml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'dev') diff --git a/dev/printers.mllib b/dev/printers.mllib index e15855ef26..9b4998c671 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -37,7 +37,7 @@ Feedback Segmenttree Unicodetable Unicode -Errors +CErrors CWarnings Bigint CUnix diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6074acea46..7c010e6a48 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -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"; -- cgit v1.2.3 From cf95f2a791c263c7aaa3b488d1b09eaafc29be2b Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 27 Jun 2016 16:30:32 +0200 Subject: closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module) For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a --- dev/printers.mllib | 2 +- dev/top_printers.ml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'dev') diff --git a/dev/printers.mllib b/dev/printers.mllib index 9b4998c671..a2a7437fb7 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -86,7 +86,7 @@ Nativecode Nativelib Cbytegen Environ -Closure +CClosure Reduction Nativeconv Type_errors diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 7c010e6a48..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")" -- cgit v1.2.3 From 3ce70f21a18cc19e720e8ac54b93652527881942 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 27 Jun 2016 18:15:07 +0200 Subject: rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cErrors.ml) --- dev/base_include | 4 ++-- dev/printers.mllib | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'dev') 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 a2a7437fb7..3165495488 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -208,7 +208,7 @@ Dn Btermdn Hints Himsg -Cerrors +ExplainErr Locality Assumptions Vernacinterp -- cgit v1.2.3