From 7cff0b6c6a492fd39640f7e73f4aa88f932fb0e2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 6 Feb 2001 00:23:22 +0000
Subject: 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
---
 parsing/termast.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'parsing/termast.ml')

diff --git a/parsing/termast.ml b/parsing/termast.ml
index 8e7cc12af2..3d72f4adcd 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
 
-- 
cgit v1.2.3