From 7ff42d43a6107dff984676902943ec32f187c40d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 13 Oct 2016 13:44:35 +0200
Subject: [pp] Add tagging function to all low-level printing calls.

The current tag system in `Pp` is generic, which implies we must choose
a tagging function when calling a printer.

For console printing there is a single choice, thus this commits adds it
a few missing cases.
---
 plugins/ssrmatching/ssrmatching.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index a34fa4cae7..4d1ac71394 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -112,7 +112,7 @@ let guard_term ch1 s i = match s.[i] with
 (* The call 'guard s i' should return true if the contents of s *)
 (* starting at i need bracketing to avoid ambiguities.          *)
 let pr_guarded guard prc c =
-  msg_with Format.str_formatter (prc c);
+  msg_with ~pp_tag:Ppstyle.pp_tag Format.str_formatter (prc c);
   let s = Format.flush_str_formatter () ^ "$" in
   if guard s (skip_wschars s 0) then pr_paren prc c else prc c
 (* More sensible names for constr printers *)
-- 
cgit v1.2.3


From cb5f55380875bb3029b051eb3acfbb912d83454b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 13 Oct 2016 14:21:22 +0200
Subject: [pp] Use more convenient pp API in ssrmatching

---
 plugins/ssrmatching/ssrmatching.ml4 | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 4d1ac71394..21606b2d65 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -112,8 +112,7 @@ let guard_term ch1 s i = match s.[i] with
 (* The call 'guard s i' should return true if the contents of s *)
 (* starting at i need bracketing to avoid ambiguities.          *)
 let pr_guarded guard prc c =
-  msg_with ~pp_tag:Ppstyle.pp_tag Format.str_formatter (prc c);
-  let s = Format.flush_str_formatter () ^ "$" in
+  let s = Pp.string_of_ppcmds (prc c) ^ "$" in
   if guard s (skip_wschars s 0) then pr_paren prc c else prc c
 (* More sensible names for constr printers *)
 let pr_constr = pr_constr
-- 
cgit v1.2.3


From a7996005f57c12ba8fbb22c61ad97ac872da9d83 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Mon, 24 Oct 2016 08:48:05 +0200
Subject: That Function is unable to create a Fixpoint equation is a user
 problem, not an anomaly

---
 plugins/funind/recdef.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 62f3071151..fa84e4ddf3 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1538,7 +1538,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
 	begin
 	  if do_observe ()
 	  then Feedback.msg_debug (str "Cannot create equation Lemma " ++ CErrors.print e)
-	  else anomaly (Pp.str "Cannot create equation Lemma")
+	  else CErrors.errorlabstrm "Cannot create equation Lemma"
+               (str "Cannot create equation lemma." ++ spc () ++ 
+                str "This may be because the function is nested-recursive.")
 	  ;
 	  true
 	end
-- 
cgit v1.2.3