diff options
| author | herbelin | 2006-10-28 19:35:09 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-28 19:35:09 +0000 |
| commit | 359e4ffe307d7d8dd250735373fc6354a58ecff5 (patch) | |
| tree | 7204cb80cb272118a7ee60e9790d91d0efd11894 /kernel/subtyping.ml | |
| parent | 8bcd34ae13010797a974b0f3c16df6e23f2cb254 (diff) | |
Extension du polymorphisme de sorte au cas des définitions dans Type.
(suppression au passage d'un cast dans constant_entry_of_com - ce
n'est pas normal qu'on force le type s'il n'est pas déjà présent mais
en même temps il semble que ce cast serve pour rafraîchir les univers
algébriques...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index c94219316b..12c7144114 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -96,7 +96,7 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = (* nparams done *) (* params_ctxt done because part of the inductive types *) (* 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)) + let cst = check_conv cst conv env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2)) in cst in @@ -164,7 +164,9 @@ let check_constant cst env msid1 l info1 cb2 spec2 = | Constant cb1 -> assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; (*Start by checking types*) - let cst = check_conv cst conv_leq env cb1.const_type cb2.const_type in + let typ1 = Typeops.type_of_constant_type env cb1.const_type in + let typ2 = Typeops.type_of_constant_type env cb2.const_type in + let cst = check_conv cst conv_leq env typ1 typ2 in let con = make_con (MPself msid1) empty_dirpath l in let cst = match cb2.const_body with @@ -186,8 +188,9 @@ 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 = type_of_inductive (mind1,mind1.mind_packets.(i)) in - check_conv cst conv_leq env arity1 cb2.const_type + let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in + let typ2 = Typeops.type_of_constant_type env cb2.const_type in + check_conv cst conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> ignore (Util.error ( "The kernel does not recognize yet that a parameter can be " ^ @@ -197,7 +200,8 @@ let check_constant cst env msid1 l info1 cb2 spec2 = assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; if cb2.const_body <> None then error () ; let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in - check_conv cst conv env ty1 cb2.const_type + let ty2 = Typeops.type_of_constant_type env cb2.const_type in + check_conv cst conv env ty1 ty2 | _ -> error () let rec check_modules cst env msid1 l msb1 msb2 = |