anchor.diff:    | Typ_uvar _ -> unknownType
     | Typ_delayed _ -> unknownType
     | Typ_unknown  _ -> unknownType
  -and getTypeFromArg (a:arg) : mlty =
  +and getTypeFromArg (c:context) (a:arg) : mlty =
   match (fst a) with
  -| Inl ty -> extractTyp ty
  +| Inl ty -> extractTyp c ty
   | Inr _ -> erasedContent 
   (* In OCaml, there are no expressions in type applications.
      Need to make similar changes when extracting the definitions of type schemes
  
positive.code:   | 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
    | 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
               | Some tys -> 
                   let mlargs = map getTypeFromArg args in
                      (MLTY_App (extractType tys) (MLTY_Tuple mlargs))
               | None -> 
                   (match  (deltaUnfold ftv ) with
                   | Some tyu ->  extracType tyu
                   | None -> unknownType
                   )
              )
  
negative.code:   | Comp cm -> extractTyp c (cm.result_typ)
  
  
  let binderIdent (bn:binder): ident =
  match bn with
  | (Inl btv,_) -> btv.v.realname
  | (Inr bvv,_) -> bvv.v.realname
  
  let extendContextWithTyVars (c:context) (idents : list<ident>) : context = failwith "extendContextWithTyVars is not implemented"
  
  let extractSigElt (c:context) (s:sigelt) : mlsig =
  match s with
  | Sig_typ_abbrev (l,bs,k,t,q,r) -> 
      let idents = List.map binderIdent bs in
      let tyDecBody = MLTD_Abbrev (extractTyp (extendContextWithTyVars c idents) t) in
       [MLS_Ty [(l.str, List.map convIdent idents , Some tyDecBody)]]
  | Sig_tycon (l,bs,k,muts,constrs,lq,r) -> [] (*this will be a list with possibly several elements, depending on the constructors. We can first ignore mutual inductives*)
  | _ -> []
  
  
  