From 376e61185dadea415d6b7d2df45dc7236e901e5b Mon Sep 17 00:00:00 2001 From: barras Date: Tue, 6 May 2008 18:31:25 +0000 Subject: checker deals with polymorphic constants and module aliases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10892 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/typeops.ml | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'checker/typeops.ml') diff --git a/checker/typeops.ml b/checker/typeops.ml index 27a3e287d..1af8b2ced 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -436,3 +436,21 @@ let check_named_ctxt env ctxt = conv_leq env j1 ty; push_named d env) ctxt ~init:env + +(* Polymorphic arities utils *) + +let check_kind env ar u = + if snd (dest_prod env ar) = Sort(Type u) then () + else failwith "not the correct sort" + +let check_polymorphic_arity env params par = + let pl = par.poly_param_levels in + let rec check_p env pl params = + match pl, params with + Some u::pl, (na,None,ty)::params -> + check_kind env ty u; + check_p (push_rel (na,None,ty) env) pl params + | None::pl,d::params -> check_p (push_rel d env) pl params + | [], _ -> () + | _ -> failwith "check_poly: not the right number of params" in + check_p env pl (List.rev params) -- cgit v1.2.3