diff options
| author | herbelin | 2008-12-31 10:57:09 +0000 |
|---|---|---|
| committer | herbelin | 2008-12-31 10:57:09 +0000 |
| commit | 0d03f17a33b43aa87bb201953e4e1a567aac6355 (patch) | |
| tree | bfb3179e3de28fee2d900b202de3a4281a062eda /kernel/subtyping.ml | |
| parent | d3c49a6e536006ff121f01303ddc0a43b4c90e23 (diff) | |
Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->
splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added
shortcuts for "fst (decompose_prod t)" and co.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11727 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 387d97de97..1f77c3e43c 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -115,8 +115,7 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = | Type _, Type _ -> (* shortcut here *) prop_sort, prop_sort | (Prop _, Type _) | (Type _,Prop _) -> error () | _ -> (s1, s2) in - check_conv cst conv_leq env - (Sign.mkArity (ctx1,s1)) (Sign.mkArity (ctx2,s2)) + check_conv cst conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) in let check_packet cst p1 p2 = @@ -210,8 +209,8 @@ let check_constant cst env msid1 l info1 cb2 spec2 = Hence they don't have to be checked again *) let t1,t2 = - if Sign.isArity t2 then - let (ctx2,s2) = Sign.destArity t2 in + if isArity t2 then + let (ctx2,s2) = destArity t2 in match s2 with | Type v when not (is_univ_variable v) -> (* The type in the interface is inferred and is made of algebraic @@ -222,13 +221,13 @@ let check_constant cst env msid1 l info1 cb2 spec2 = | Type u when not (is_univ_variable u) -> (* Both types are inferred, no need to recheck them. We cheat and collapse the types to Prop *) - Sign.mkArity (ctx1,prop_sort), Sign.mkArity (ctx2,prop_sort) + mkArity (ctx1,prop_sort), mkArity (ctx2,prop_sort) | Prop _ -> (* The type in the interface is inferred, it may be the case that the type in the implementation is smaller because the body is more reduced. We safely collapse the upper type to Prop *) - Sign.mkArity (ctx1,prop_sort), Sign.mkArity (ctx2,prop_sort) + mkArity (ctx1,prop_sort), mkArity (ctx2,prop_sort) | Type _ -> (* The type in the interface is inferred and the type in the implementation is not inferred or is inferred but from a |