From 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Thu, 19 Jan 2006 22:34:29 +0000
Subject: Imported Upstream version 8.0pl3

---
 pretyping/coercion.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'pretyping/coercion.ml')

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index f214388f..be78eb2c 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: coercion.ml,v 1.38.6.1 2004/07/16 19:30:44 herbelin Exp $ *)
+(* $Id: coercion.ml,v 1.38.6.2 2005/11/29 21:40:52 letouzey Exp $ *)
 
 open Util
 open Names
@@ -60,10 +60,6 @@ let inh_pattern_coerce_to loc pat ind1 ind2 =
 (* appliquer le chemin de coercions p à hj *)
 
 let apply_coercion env p hj typ_cl =
-  if !compter then begin
-    nbpathc := !nbpathc +1; 
-    nbcoer := !nbcoer + (List.length p)
-  end;
   try 
     fst (List.fold_left
            (fun (ja,typ_cl) i -> 
-- 
cgit v1.2.3