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 /mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | |
| parent | aa13fe8081c0d28478e5464bfdb52e44b1df6945 (diff) | |
| parent | 760351d5864d5f98d75f310ace6b37bda7a471a9 (diff) | |
Merge pull request #48 from ejgallego/pp_cleanup_fix
Compatibility with latest Coq trunk.
Diffstat (limited to 'mathcomp/ssreflect/plugin/trunk/ssreflect.ml4')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 7 |
1 files changed, 6 insertions, 1 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 |