From 94edcde5a3f4826defe7290bf2a0914c860a85ae Mon Sep 17 00:00:00 2001
From: Pierre
Date: Sat, 11 Jan 2014 09:22:47 +0100
Subject: 'Pretty' printer for wf_paths

---
 dev/top_printers.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 31c5e608a9..857a989dc7 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -59,6 +59,14 @@ let pprecarg = function
      str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
 let ppwf_paths x = pp (Rtree.pp_tree pprecarg x)
 
+let pprecarg = function
+  | Declarations.Norec -> str "Norec"
+  | Declarations.Mrec (mind,i) ->
+     str "Mrec[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
+  | Declarations.Imbr (mind,i) ->
+     str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]"
+let ppwf_paths x = pp (Rtree.pp_tree pprecarg x)
+
 (* term printers *)
 let rawdebug = ref false
 let ppevar evk = pp (str (Evd.string_of_existential evk))
-- 
cgit v1.2.3