anchor.diff:    | Typ_btvar _ -> extractType' c (Typ_app (liftType' ft, []))
     | Typ_const _ -> extractType' c (Typ_app (liftType' ft, []))
     | Typ_fun (bb, cm) -> 
  -        let codomain = (extractComp  c cm) in 
  -        if  (codomain = erasedContent) then erasedContent else  (curry (List.map (extractBinder c) bb) codomain)
  -  | Typ_refine (bv,ty) -> extractType ty
  +        (let codomain = (extractComp  c cm) in 
  +        if  (codomain = erasedContent) then erasedContent else  (curry (List.map (extractBinder c) bb) codomain))
  +  | Typ_refine (bv,ty) -> extractTyp c ty
     | Typ_app (ty, arrgs) ->
       (match ty.n with
           | Typ_btvar btv -> (if (contains c btv) then MLTY_Var (convIdent btv.v.realname) else unknownType)
               (*the args are thrown away, because in OCaml, type variables have type Type and not something like -> .. -> .. Type *)
           | Typ_const ftv -> 
  -            (match  (isTypeScheme  ftv)  with
  +            (match  (isTypeScheme ftv.v c)  with
                | Some tys -> 
  -                 let mlargs = map getTypeFromArg args in
  -                    (MLTY_App (extractType tys) (MLTY_Tuple mlargs))
  +                 let mlargs = List.map (getTypeFromArg c) arrgs in
  +                    (MLTY_App (extractTyp c tys, MLTY_Tuple mlargs))
                | None -> 
  -                 (match  (deltaUnfold ftv ) with
  -                 | Some tyu ->  extracType tyu
  +                 (match  (deltaUnfold ftv.v c) with
  +                 | Some tyu ->  extractTyp c tyu
                    | None -> unknownType
                    )
               )
  
positive.code:   | Typ_uvar _ -> unknownType
    | Typ_delayed _ -> unknownType
    | Typ_unknown  _ -> unknownType
  and getTypeFromArg (a:arg) : mlty =
  match (fst a) with
  | Inl ty -> extractTyp ty
  | Inr _ -> erasedContent 
  (* In OCaml, there are no expressions in type applications.
     Need to make similar changes when extracting the definitions of type schemes
  
negative.code: (*assuming that btvar includes the name of the variable*)
  type context = env
  (*is there an F# library of associative lists?*)
  let contains (c:context) (b:btvar) = failwith "contains is undefined"
  
  
  let deltaUnfold (i : lident) (c: context) : (option<typ>) = failwith "deltaUnfold is undefined"
  
  (*The thesis defines a type scheme as "something that becomes a type when enough arguments (possibly none?) are applied to it" ,  e.g. vector, list.
      I guess in F*, these include Inductive types and type abbreviations  *)
  let isTypeScheme (i : lident) (c: context) : (option<typ>) =  failwith "isTypeScheme is undefined"
  
  let liftType' (t:typ') : typ = failwith "liftType is undefined"
  
  (*the \hat{\epsilon} function in the thesis (Sec. 3.3.5) *)
  let rec extractType' (c:context) (ft:typ') : mlty = 
  