From bd1e31d0e3f20e82778306bd27e0b0f8cd475757 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 12 Feb 2005 11:20:58 +0000
Subject: Ajout Print Canonical Structures

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6711 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_basevernac.ml4 |  1 +
 parsing/g_vernacnew.ml4  |  1 +
 parsing/prettyp.ml       | 14 ++++++++++----
 parsing/prettyp.mli      |  1 +
 4 files changed, 13 insertions(+), 4 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 79b0e26fc..a8f46a12b 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -191,6 +191,7 @@ GEXTEND Gram
       | IDENT "Coercions" -> PrintCoercions
       | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
          -> PrintCoercionPaths (s,t)
+      | IDENT "Canonical"; IDENT "Structures" -> PrintCanonicalStructures
       | IDENT "Tables" -> PrintTables
       | "Proof"; qid = global -> PrintOpaqueName qid
       | IDENT "Hint" -> PrintHintGoal
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index e920352d1..5b0350f82 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -579,6 +579,7 @@ GEXTEND Gram
       | IDENT "Coercions" -> PrintCoercions
       | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
          -> PrintCoercionPaths (s,t)
+      | IDENT "Canonical"; IDENT "Structures" -> PrintCanonicalStructures
       | IDENT "Tables" -> PrintTables
 (* Obsolete: was used for cooking V6.3 recipes ??
       | IDENT "Proof"; qid = global -> PrintOpaqueName qid
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 ())
+
 (*************************************************************************)
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 3af935d08..20429cd3d 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -57,6 +57,7 @@ val print_graph : unit -> std_ppcmds
 val print_classes : unit -> std_ppcmds
 val print_coercions : unit -> std_ppcmds
 val print_path_between : Classops.cl_typ -> Classops.cl_typ -> std_ppcmds
+val print_canonical_structures : unit -> std_ppcmds
 
 val inspect : int -> std_ppcmds
 
-- 
cgit v1.2.3