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/evarconv.ml | |
| parent | 6497f27021fec4e01f2182014f2bb1989b4707f9 (diff) | |
Imported Upstream version 8.0pl3upstream/8.0pl3
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 27 |
1 files changed, 11 insertions, 16 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0ee95a0f..2264f82b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarconv.ml,v 1.44.6.2 2004/11/26 23:51:39 herbelin Exp $ *) +(* $Id: evarconv.ml,v 1.44.6.3 2005/11/29 21:40:52 letouzey Exp $ *) open Util open Names @@ -380,21 +380,16 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = (new_isevar isevars env dloc (substl ks b)) :: ks) [] bs in - if (list_for_all2eq - (fun u1 u -> evar_conv_x env isevars CONV u1 (substl ks u)) - us2 us) - & - (list_for_all2eq - (fun x1 x -> evar_conv_x env isevars CONV x1 (substl ks x)) - params1 params) - & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1) - & (evar_conv_x env isevars CONV c1 (applist (c,(List.rev ks)))) - then - (*TR*) (if !compter then (nbstruc:=!nbstruc+1; - nbimplstruc:=!nbimplstruc+(List.length ks);true) - else true) - else false - + (list_for_all2eq + (fun u1 u -> evar_conv_x env isevars CONV u1 (substl ks u)) + us2 us) + & + (list_for_all2eq + (fun x1 x -> evar_conv_x env isevars CONV x1 (substl ks x)) + params1 params) + & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1) + & (evar_conv_x env isevars CONV c1 (applist (c,(List.rev ks)))) + let the_conv_x env isevars t1 t2 = evar_conv_x env isevars CONV t1 t2 let the_conv_x_leq env isevars t1 t2 = evar_conv_x env isevars CUMUL t1 t2 |