anchor.diff:  | Inl ty -> extractTyp c ty
   | Inr _ -> erasedContent 
   
  -(* Return the new context, where this binder might be in scope. Actually this code be reverted back to the old, less complicated state
  -   where c.allowTypeVars was always assumed to be false. *)
  -and extractBinderType  (c:context) (bn : binder): mlty * context =
  +and extractBinderType  (c:context) (bn : binder): mlty =
   match bn with
  -| (Inl btv,_) ->
  -      let k = (btv.sort) in 
  -      let newC = (match k.n with
  -                 | Kind_type -> (if c.allowTypeVars then (extendContext c [btv.v.realname] [] c.allowTypeVars) else c)
  -                 | _ ->  c)
  -       in  (extractKind (disallowTypeVars c) (btv.sort), newC)
  -| (Inr bvv,_) -> (extractTyp (disallowTypeVars c) (bvv.sort), c)
  -
  -and extractBindersTypes  (c:context) (bs : list<binder>): list<mlty> * context =
  -match bs with
  -| (h::tl) ->  let (t,newC) = extractBinderType c h in
  -               let (lt, newNewC) = extractBindersTypes newC tl in
  -               ((t::lt),newNewC)
  -| [] -> ([], c)
  -
  +| (Inl btv,_) -> (extractKind c (btv.sort))
  +| (Inr bvv,_) -> (extractTyp c (bvv.sort))
  +
  +and extractBindersTypes  (c:context) (bs : list<binder>): list<mlty> =
  +  List.map (extractBinderType c) bs
   and extractTyp  (c:context) (ft:typ) : mlty = extractType' c (ft.n)
   and extractKind (c:context) (ft:knd) : mlty = erasedContent
   and extractComp  (c:context) (ft:comp) : mlty = extractComp' c (ft.n) 
  
positive.code:             )
  
    | Typ_fun (bs, codomain) -> 
          let (bts, newC) = extractBindersTypes c bs in
          (let codomainML = (extractComp  newC codomain) in 
          if  (codomainML = erasedContent) 
          then erasedContent 
          else  (curry bts codomainML))
  
negative.code: 
  (*similar to the definition of the second part of \hat{\epsilon} in page 110*)
  (* \pi_1 of returned value is the exported constant*)
  let extractSigElt (c:context) (s:sigelt) :  option<(mlsig1)> =
  match s with
  | Sig_typ_abbrev (l,bs,_,t,_,_) -> 
      let identsPP = List.map binderPPnames bs in
      let newContext = (extendContext c bs) in
      let tyDecBody = MLTD_Abbrev (extractTyp newContext t) in
              //printfn "type is %A\n" (t);
       Some (MLS_Ty [(mlsymbolOfLident l, List.map (fun x -> prependTick (convIdent x)) identsPP , Some tyDecBody)])
       (*type l idents = tyDecBody*)
  
  | Sig_bundle _ -> 
      let ind = parseFirstInductiveType s in
      let identsPP = List.map binderPPnames ind.tyBinders in
      let newContext = (extendContext c ind.tyBinders) in
      let nIndices = numIndices ind.k.n ind.tyName.ident.idText in
      let tyDecBody = MLTD_DType (List.map (extractCtor newContext) ind.constructors) in
            Some (MLS_Ty [(lident2mlsymbol ind.tyName, List.append (List.map (fun x -> prependTick (convIdent x)) identsPP) (dummyIndexIdents nIndices)  , Some tyDecBody)])
  | _ -> None
  
  let rec extractTypeDefnsAux (c: context) (sigs:list<sigelt>) : list<option<mlsig1>> =
    List.map  (extractSigElt c) sigs
   
  let pruneNones (l : list<option<'a>>) : list<'a> =
  List.fold (fun ll x -> match x with 
                        | Some xs -> xs::ll
                        | None -> ll) [] l
  
  let extractTypeDefns (sigs:list<sigelt>) (e: env): list<mlsig1> =
     pruneNones (extractTypeDefnsAux e sigs)
  
  