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

1 files changed, 18 insertions, 0 deletions

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)