anchor.diff:     In particular, the definition of a type constant is not needed when translating references to it.
      However, enough info is needed to determine whether a type constant is a type scheme. add that.
   *)
  -type context = {
  -    tyVars : list<ident>;
  -    tyConstants : list<lident>;
  -    allowTypeVars : bool
  -}
  -
  -let emptyContext : context = {tyVars=[]; tyConstants =[]; allowTypeVars=true}
  +type context = env
   
   (* vars in tyVars will have type Type, irrespective of that types they had in F*. This is to match the limitations of  OCaml*)
  -let extendContext (c:context) (tyVars : list<ident>) (tyConsts : list<lident>) (alowTypeVars_ : bool ): context = 
  -    { tyVars = List.append c.tyVars tyVars; tyConstants = List.append c.tyConstants tyConsts; allowTypeVars = alowTypeVars_}
  -
  -let disallowTypeVars (c:context) : context = extendContext c [] [] false
  -
  -let contains (c:context) (b:btvar) : bool =     
  -    List.contains ( b.v.realname.idText)  (List.map (fun x -> x.idText) c.tyVars) (*needed for sh, its ppname is _, and range is 0*)
  -    || List.contains (b.v.realname.idRange)  (List.map (fun x -> x.idRange) c.tyVars) (*needed for inductive constructors. names often have extra things appended*)
  +let extendContext (c:env) (tyVars : list<binder>) : env = 
  +  List.fold push_local_binding c (List.map binding_of_binder tyVars)
  +
  +
  +let contains (c:context) (b:btvar) : bool = 
  +  try (let _ = (lookup_btvar c b) in true)
  +  with
  +   | _ -> false
   
   let deltaUnfold (i : lident) (c: context) : (option<typ>) = None (*FIX!!*)
   
  
positive.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<(lident * mlsig1)> =
  match s with
  | Sig_typ_abbrev (l,bs,_,t,_,_) -> 
      let identsPP = List.map binderPPnames bs in
      let identsReal = List.map binderRealnames bs in
              //printfn "binders are %A\n" (identsReal);
      let newContext = (extendContext c identsReal [l] true) in
      let tyDecBody = MLTD_Abbrev (extractTyp newContext t) in
              //printfn "type is %A\n" (t);
       Some (l, 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 identsReal = List.map binderRealnames ind.tyBinders in
              // printfn "binders are %A\n" (identsReal);
      let newContext = (extendContext c identsReal [ind.tyName] false) in
      let nIndices = numIndices ind.k.n ind.tyName.ident.idText in
      let tyDecBody = MLTD_DType (List.map (extractCtor newContext) ind.constructors) in
            Some (ind.tyName, 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<mlsig1> =
      match sigs with
      | hsig::tlsigs ->
          (match extractSigElt c hsig with
          | Some (exportedConst, mls) ->  
                  let nc = extendContext c [] [exportedConst] true in
                  mls::(extractTypeDefnsAux nc tlsigs)
          | None -> (extractTypeDefnsAux c tlsigs)
          )
      | _ -> []
  
  let extractTypeDefns (sigs:list<sigelt>) (e: env): list<mlsig1> =
     extractTypeDefnsAux emptyContext sigs
  
  
negative.code:             )
  
    | Typ_fun (bs, codomain) -> 
          let bts = extractBindersTypes c bs in
          (let codomainML = (extractComp  c codomain) in 
          if  (codomainML = erasedContent) 
          then erasedContent 
          else  (curry bts codomainML))
  