+let rec fomega_subst k t1 =
+ function
+ | Var n ->
+ if k=n then t1
+ else if n < k then Var n
+ else Var (n-1)
+ | Top -> Top
+ | TConst ref -> TConst ref
+ | Unit -> Unit
+ | Arrow (ty1,ty2) -> Arrow (fomega_subst k t1 ty1, fomega_subst (k+1) t1 ty2)
+ | Skip t -> Skip (fomega_subst (k+1) t1 t)
+ | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t)
+ | TAppl args -> TAppl (List.map (fomega_subst k t1) args)
+
+let fomega_lookup status ref = snd (ReferenceMap.find ref status#extraction_db)
+
+let rec fomega_whd status ty =
+ match ty with
+ | TConst r ->
+ (match fomega_lookup status r with
+ None -> ty
+ | Some ty -> fomega_whd status ty)
+ | TAppl (TConst r::args) ->
+ (match fomega_lookup status r with
+ None -> ty
+ | Some ty -> fomega_whd status (List.fold_right (fomega_subst 1) args ty))
+ | _ -> ty
+