From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- kernel/subtyping.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'kernel/subtyping.ml') diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 94251d90..bbc89e39 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtyping.ml 7639 2005-12-02 10:01:15Z gregoire $ i*) +(*i $Id: subtyping.ml 8845 2006-05-23 07:41:58Z herbelin $ i*) (*i*) open Util @@ -89,14 +89,15 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = (* nf_arity later *) (* user_lc ignored *) (* user_arity ignored *) - let cst = check_conv cst conv_sort env p1.mind_sort p2.mind_sort in check (fun p -> p.mind_nrealargs); (* kelim ignored *) (* listrec ignored *) (* finite done *) (* nparams done *) (* params_ctxt done *) - let cst = check_conv cst conv env p1.mind_nf_arity p2.mind_nf_arity in + (* Don't check the sort of the type if polymorphic *) + let cst = check_conv cst conv env (type_of_inductive (mib1,p1)) (type_of_inductive (mib2,p2)) + in cst in let check_cons_types i cst p1 p2 = @@ -181,7 +182,7 @@ let check_constant cst env msid1 l info1 cb2 spec2 = "name.") ; assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; if cb2.const_body <> None then error () ; - let arity1 = mind1.mind_packets.(i).mind_user_arity in + let arity1 = type_of_inductive (mind1,mind1.mind_packets.(i)) in check_conv cst conv_leq env arity1 cb2.const_type | IndConstr (((kn,i),j) as cstr,mind1) -> Util.error ("The kernel does not recognize yet that a parameter can be " ^ -- cgit v1.2.3