let dummy = C.Sort C.Prop in
(*CSC: to be moved in cicSubstitution? *)
let rec subst_inductive_type_with_dummy _ = function
+ | C.Meta (_,(_,C.Irl _)) as x -> x
+ | C.Meta (i,(lift,C.Ctx ls)) ->
+ C.Meta (i,(lift,C.Ctx
+ (List.map (subst_inductive_type_with_dummy ()) ls)))
| C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))) when NUri.eq uri' uri -> dummy
| C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0,lno))))::tl)
when NUri.eq uri' uri ->
with Failure _ ->
raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n
^" under: " ^ NCicPp.ppcontext ~metasenv ~subst context))))
- | C.Sort (C.Type [false,u]) -> C.Sort (C.Type [true, u])
+ | C.Sort (C.Type ([false,u] as univ)) ->
+ if NCicEnvironment.is_declared univ then
+ C.Sort (C.Type [true, u])
+ else
+ raise (TypeCheckerFailure (lazy ("undeclared universe " ^
+ NUri.string_of_uri u)))
| C.Sort (C.Type _) ->
raise (AssertFailure (lazy ("Cannot type an inferred type: "^
NCicPp.ppterm ~subst ~metasenv ~context t)))