Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_basevernac.ml4

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

1 files changed, 11 insertions, 3 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 710a723e36..0b190db0e8 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -138,9 +138,17 @@ let coe_of_reference = function
   | EvarRef _ -> raise Not_found
   | x -> x
 
-let hide_coercion r =
-  let _,coe_info = coercion_info (coe_of_reference r) in
-  if coe_info.coe_hide then None else Some coe_info.coe_param
+let hide_coercion coe =
+  let _,coe_info = coercion_info coe in
+  if coe_info.coe_hide then Some coe_info.coe_param else None
+
+let set_coercion_visibility b coe =
+  let _,coe_info = coercion_info coe in
+  coe_info.coe_hide <- not b
+
+let is_coercion_visible coe = 
+  let _,coe_info = coercion_info coe in
+  not coe_info.coe_hide
 
 let coercion_params coe_info = coe_info.coe_param