in
CicSubstitution.lift_meta l ty, subst', metasenv'
(* TASSI: CONSTRAINT *)
- | C.Sort (C.Type t) ->
- let t' = CicUniv.fresh() in
+ | 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 s2,subst,metasenv
| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
(* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
- let t' = CicUniv.fresh() in
+ let t' = CicUniv.fresh() in
if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
assert false ; (* not possible, error in CicUniv *)
C.Sort (C.Type t'),subst,metasenv