diff options
| author | Enrico | 2016-06-01 14:41:40 +0200 |
|---|---|---|
| committer | Enrico | 2016-06-01 14:41:40 +0200 |
| commit | 5be3b636eec8a376828f8600c0f7e7a1a5fc271c (patch) | |
| tree | f09d276327d7e961ab0e7ee0ce78a8ec8abc5657 | |
| parent | aa13fe8081c0d28478e5464bfdb52e44b1df6945 (diff) | |
| parent | 760351d5864d5f98d75f310ace6b37bda7a471a9 (diff) | |
Merge pull request #48 from ejgallego/pp_cleanup_fix
Compatibility with latest Coq trunk.
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 7 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 | 5 |
2 files changed, 10 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 index 579a742..2ee0d97 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 @@ -23,6 +23,7 @@ let frozen_lexer = CLexer.freeze () ;; open Names open Pp +open Feedback open Pcoq open Pcoq.Prim open Pcoq.Constr @@ -99,6 +100,10 @@ let errorstrm = Errors.errorlabstrm "ssreflect" let loc_error loc msg = Errors.user_err_loc (loc, msg, str msg) let anomaly s = Errors.anomaly (str s) +(* Compatibility with Coq 8.6 *) +let ppnl = msg_info +let msgnl = msg_info + (** look up a name in the ssreflect internals module *) let ssrdirpath = make_dirpath [id_of_string "ssreflect"] let ssrqid name = make_qualid ssrdirpath (id_of_string name) @@ -142,7 +147,7 @@ let is_ssr_loaded () = (* 0 cost pp function. Active only if env variable SSRDEBUG is set *) (* or if SsrDebug is Set *) let pp_ref = ref (fun _ -> ()) -let ssr_pp s = pperrnl (str"SSR: "++Lazy.force s) +let ssr_pp s = msg_error (str"SSR: "++Lazy.force s) let _ = try ignore(Sys.getenv "SSRDEBUG"); pp_ref := ssr_pp with Not_found -> () let _ = Goptions.declare_bool_option diff --git a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 index e508ab7..f04a910 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4 @@ -57,10 +57,13 @@ let dummy_loc = Loc.ghost let errorstrm = Errors.errorlabstrm "ssreflect" let loc_error loc msg = Errors.user_err_loc (loc, msg, str msg) +(* Compatibility with Coq 8.6 *) +let ppnl = Feedback.msg_info + (* 0 cost pp function. Active only if env variable SSRDEBUG is set *) (* or if SsrDebug is Set *) let pp_ref = ref (fun _ -> ()) -let ssr_pp s = pperrnl (str"SSR: "++Lazy.force s) +let ssr_pp s = Feedback.msg_error (str"SSR: "++Lazy.force s) let _ = try ignore(Sys.getenv "SSRDEBUG"); pp_ref := ssr_pp with Not_found -> () let debug b = if b then pp_ref := ssr_pp else pp_ref := fun _ -> () |