anchor.diff:  let unknownType : mlty = MLTY_Var  ("Obj.t", 0)
   
   let convRange (r:Range.range) : int = 0 (*FIX!!*)
  -let convIdent (id:ident) : mlident = (id.idText (*FIX!! these names are of the form _n_m*) ,(convRange id.idRange))
  +let convIdent (id:ident) : mlident = (id.idText ,(convRange id.idRange))
       
   (* This is all the context is needed for extracting F* types to OCaml.
      In particular, the definition of a type constant is not needed when translating references to it.
  
positive.code: 
  let emptyContext : context = {tyVars=[]; tyConstants =[]}
  
  (*is there an F# library of associative lists?*)
  let contains (c:context) (b:btvar) = List.contains b.v.ppname (*why not ppname?*) c.tyVars
  
  let deltaUnfold (i : lident) (c: context) : (option<typ>) = None (*FIX!!*)
  
negative.code: 
  let lident2mlpath (l:lident) : mlpath =
    (List.map (fun x -> x.idText) l.ns, l.ident.idText)
  
  
  (*the \hat{\epsilon} function in the thesis (Sec. 3.3.5) *)
  let rec extractType' (c:context) (ft:typ') : mlty = 
  (* first \beta, \iota and \zeta reduces ft. Since F* does not have SN, one has to be more careful for the termination argument.
  