affichage classes et coercions

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

2 files changed, 24 insertions, 5 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index dc398cc367..b8a95a0bcf 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -52,10 +52,16 @@ type inheritance_path = int list
 
 let cLASSES = (ref [] : (int * (cl_typ * cl_info_typ)) list ref)
 
+let classes () = !cLASSES
+
 let cOERCIONS = (ref [] : (int * (coe_typ * coe_info_typ)) list ref)
 
+let coercions () = !cOERCIONS
+
 let iNHERITANCE_GRAPH = (ref [] : ((int * int) * inheritance_path) list ref) 
 
+let inheritance_graph () = !iNHERITANCE_GRAPH
+
 let freeze () = (!cLASSES,!cOERCIONS, !iNHERITANCE_GRAPH)
 
 let unfreeze (fcl,fco,fig) = 
@@ -229,9 +235,16 @@ let coe_value i =
 
 (* pretty-print functions are now in Pretty *)
 (* rajouter une coercion dans le graphe *)
+
+let path_printer = ref (fun _ -> [< 'sTR "<a class path>" >] 
+                        : (int * int) * inheritance_path -> std_ppcmds)
+
+let install_path_printer f = path_printer := f
  
+let print_path x = !path_printer x
+
 let message_ambig l = 
-  [< 'sTR"Ambiguous paths : ";
+  [< 'sTR"Ambiguous paths:"; 'sPC;
      prlist_with_sep pr_fnl (fun ijp -> print_path ijp) l >]
 
 (* add_coercion_in_graph : int * int * int -> unit 
@@ -276,8 +289,8 @@ let add_coercion_in_graph (ic,source,target) =
 	 end)
       old_iNHERITANCE_GRAPH 
   end;
-  if ((!ambig_paths) <> []) & is_mes_ambig() then 
-    pPNL (message_ambig (!ambig_paths))
+  if (!ambig_paths <> []) & is_mes_ambig() then 
+    pPNL (message_ambig !ambig_paths)
 
 let add_new_coercion_in_graph ((coef,xf),cls,clt) =
   let is,_ = class_info cls in
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 709b26b85e..26188c8535 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -37,9 +37,11 @@ type coe_info_typ = {
   cOE_ISID : bool;
   cOE_PARAM : int }
 
-
 type inheritance_path = int list
 
+val inheritance_graph : unit -> ((int * int) * inheritance_path) list
+val classes : unit -> (int * (cl_typ * cl_info_typ)) list
+val coercions : unit -> (int * (coe_typ * coe_info_typ)) list
 
 val cte_of_constr : constr -> cte_typ
 val class_info : cl_typ -> (int * cl_info_typ)
@@ -61,5 +63,9 @@ val arity_sort : constr -> int
 val fully_applied : identifier -> int -> int -> unit
 val stre_of_cl : cl_typ -> strength
 val add_new_class : (cl_typ * string * strength * int) -> unit
-val add_new_coercion_in_graph : (coe_typ * coe_info_typ) * cl_typ * cl_typ -> unit
+val add_new_coercion_in_graph : 
+  (coe_typ * coe_info_typ) * cl_typ * cl_typ -> unit
 val add_coercion_in_graph : int * int * int -> unit
+
+val install_path_printer : 
+  ((int * int) * inheritance_path -> std_ppcmds) -> unit