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, 7 insertions, 5 deletions

diff --git a/parsing/termast.ml b/parsing/termast.ml
index 8e7cc12af..3d72f4adc 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -155,11 +155,13 @@ let rec skip_coercion dest_ref (f,args as app) =
     try
       match dest_ref f with
 	| Some r ->
-	    let n = Classops.coercion_params r in
-	    if n >= List.length args then app
-	    else (* We skip a coercion *)
-	      let _,fargs = list_chop n args in
-	      skip_coercion dest_ref (List.hd fargs,List.tl fargs)
+	    (match Classops.hide_coercion r with
+	       | Some n ->
+		   if n >= List.length args then app
+		   else (* We skip a coercion *)
+		     let _,fargs = list_chop n args in
+	       	     skip_coercion dest_ref (List.hd fargs,List.tl fargs)
+	       | None -> app)
 	| None -> app
     with Not_found -> app