- let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
- let subst',metasenv' =
- check_metasenv_consistency n subst metasenv context canonical_context l
- in
- CicSubstitution.lift_meta l ty, subst', metasenv'
- | C.Sort s ->
- C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
- subst,metasenv
- | C.Implicit _ -> raise (Impossible 21)
+ (try
+ let (canonical_context, term) = CicUtil.lookup_subst n subst in
+ let subst,metasenv =
+ check_metasenv_consistency n subst metasenv context
+ canonical_context l
+ in
+ type_of_aux subst metasenv context (CicSubstitution.lift_meta l term)
+ with CicUtil.Subst_not_found _ ->
+ let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
+ let subst,metasenv =
+ check_metasenv_consistency n subst metasenv context
+ canonical_context l
+ in
+ CicSubstitution.lift_meta l ty, subst, metasenv)
+ (* TASSI: CONSTRAINT *)
+ | C.Sort (C.Type t) ->
+ let t' = CicUniv.fresh() in
+ if not (CicUniv.add_gt t' t ) then
+ assert false (* t' is fresh! an error in CicUniv *)
+ else
+ C.Sort (C.Type t'),subst,metasenv
+ (* TASSI: CONSTRAINT *)
+ | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv
+ | C.Implicit _ -> raise (AssertFailure "21")