Ajout Print Canonical Structures

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6711 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 4 deletions

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index bbbbc3180..50347df03 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -27,6 +27,7 @@ open Printer
 open Printmod
 open Libnames
 open Nametab
+open Recordops
 
 (*********************)
 (** Basic printing   *)
@@ -593,10 +594,10 @@ let print_class i =
   pr_class cl
   
 let print_path ((i,j),p) = 
-  (str"[" ++ 
-     prlist_with_sep pr_semicolon print_coercion_value p ++
-     str"] : " ++ print_class i ++ str" >-> " ++
-     print_class j)
+  hov 2 (
+    str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++
+    str"] : ") ++
+  print_class i ++ str" >-> " ++ print_class j
 
 let _ = Classops.install_path_printer print_path
 
@@ -627,4 +628,9 @@ let print_path_between cls clt =
   in
   print_path ((i,j),p)
 
+let print_canonical_structures () =
+  prlist_with_sep pr_fnl (fun ((r1,r2),o) -> 
+    prterm o.o_DEF ++ str ": " ++ pr_global r1 ++ str " >-> " ++ pr_global r2)
+    (canonical_structures ())
+
 (*************************************************************************)