Débogage discharge des coercions; nettoyage

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

2 files changed, 12 insertions, 9 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 76925e23e7..de1205a028 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -246,11 +246,8 @@ let string_of_class = function
 (* coercion_value : int -> unsafe_judgment * bool *)
 
 let coercion_value i = 
-  let (coe,{ coe_is_identity = b }) = coercion_info_from_index i in
-  let env = Global.env () in
-  let v = constr_of_reference Evd.empty env coe in
-  let j = Retyping.get_judgment_of env Evd.empty v in
-  (j,b)
+  let { coe_value = j; coe_is_identity = b } = snd (coercion_info_from_index i)
+  in (j,b)
 
 (* pretty-print functions are now in Pretty *)
 (* rajouter une coercion dans le graphe *)
@@ -312,6 +309,8 @@ let add_coercion_in_graph (ic,source,target) =
   if (!ambig_paths <> []) && is_verbose () && is_mes_ambig() then 
     pPNL (message_ambig !ambig_paths)
 
+type coercion = (coe_typ * coe_info_typ) * cl_typ * cl_typ
+
 let cache_coercion (_,((coe,xf),cls,clt)) =
   let is,_ = class_info cls in
   let it,_ = class_info clt in
@@ -342,11 +341,11 @@ let declare_coercion coef v stre isid cls clt ps =
 	cls, clt))
 
 let coercion_strength v = v.coe_strength
+let coercion_identity v = v.coe_is_identity
+
 (* For printing purpose *)
 let get_coercion_value v = v.coe_value.uj_val
 
 let classes () = !class_tab
 let coercions () = !coercion_tab
 let inheritance_graph () = !inheritance_graph
-
-
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index fc0cc1de22..4b52616476 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -92,12 +92,16 @@ val lookup_path_to_fun_from : cl_index -> inheritance_path
 val lookup_path_to_sort_from : cl_index -> inheritance_path
 
 (*i Pour le discharge *)
+type coercion = (coe_typ * coe_info_typ) * cl_typ * cl_typ
+
 open Libobject
 val inClass : (cl_typ * cl_info_typ) -> Libobject.obj
 val outClass : Libobject.obj -> (cl_typ * cl_info_typ)
-val inCoercion : (coe_typ * coe_info_typ) * cl_typ * cl_typ -> Libobject.obj
-val outCoercion : Libobject.obj -> (coe_typ * coe_info_typ) * cl_typ * cl_typ
+val inCoercion : coercion -> Libobject.obj
+val outCoercion : Libobject.obj -> coercion
 val coercion_strength : coe_info_typ -> strength
+val coercion_identity : coe_info_typ -> bool
+val coercion_params : coe_info_typ -> int
 (*i*)
 
 (*i Crade *)