diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
| commit | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (patch) | |
| tree | fbb91e2f74c73bb867ab62c58f248a704bbe6dec /pretyping/coercion.ml | |
| parent | 6497f27021fec4e01f2182014f2bb1989b4707f9 (diff) | |
Imported Upstream version 8.0pl3upstream/8.0pl3
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 6 |
1 files changed, 1 insertions, 5 deletions
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 -> |