anchor.diff:  
           | _ -> mlAppExpr
   
  -let check_pats_for_ite (l:list<(pat * option<term> * term)>) :(bool * option<term> * option<term>) =
  -    let def = false, None, None in
  -    if List.length l <> 2 then def
  -    else
  -        let (p1, w1, e1) = List.hd l in
  -        let (p2, w2, e2) = List.hd (List.tl l) in
  -        match (w1, w2, p1.v, p2.v) with
  -            | (None, None, Pat_constant (Const_bool true), Pat_constant (Const_bool false)) -> true, Some e1, Some e2
  -            | (None, None, Pat_constant (Const_bool false), Pat_constant (Const_bool true)) -> true, Some e2, Some e1
  -            | _ -> def
  -
  -type univ = 
  -    | Term
  -    | UZero
  -    | UPlus
  -
  -let predecessor = function
  -    | Term -> failwith "Impossible"
  -    | UZero -> Term
  -    | UPlus -> UZero
  -     
  -let rec univ t = 
  -    match (SS.compress t).n with 
  -        | Tm_delayed _
  -        | Tm_unknown -> 
  -          failwith "Impossible"
  -
  -        | Tm_constant _ -> 
  -          Term
  -
  -        | Tm_bvar x 
  -        | Tm_name x ->
  -          predecessor <| univ x.sort 
  -
  -        | Tm_fvar fv -> 
  -          predecessor <| univ fv.fv_name.ty
  -
  -        | Tm_ascribed(_, t, _) -> 
  -          predecessor <| univ t
  -
  -        | Tm_type _ -> 
  -          UPlus
  -
  -        | Tm_uvar (_, t) -> 
  -          predecessor <| univ t
  -           
  -        | Tm_uinst(t, _) -> 
  -          univ t
  -
  -        | Tm_refine(x, _) -> 
  -          predecessor <| univ t
  -
  -        | Tm_arrow(bs, c) -> 
  -          univ (U.comp_result c)
  -
  -        | Tm_abs(_, _, Some c) -> 
  -          predecessor <| univ c.res_typ
  -       
  -        | Tm_abs(bs, body, None) -> 
  -          univ body
  -
  -        | Tm_let(_, body) -> 
  -          univ body
  -
  -        | Tm_match(_, branches) -> 
  -          begin match branches with 
  -            | (_, _, e)::_ -> univ e
  -            | _ -> failwith "Empty branches"
  -          end
  -
  -        | Tm_meta(t, _) -> 
  -          univ t
  -
  -        | Tm_app(head, _) -> 
  -          univ head
  -
  -let is_type t = match univ t with 
  -    | Term -> false
  -    | _ -> true
  -
  -let is_type_binder x = 
  -    match univ (fst x).sort with 
  -    | Term -> failwith "Impossible"
  -    | UZero -> false
  -    | UPlus -> true
  -
  +
  +//The main extraction function
   let rec check_term (g:env) (t:term) (f:e_tag) (ty:mlty) :  (mlexpr * mlty) =
       // debug g (fun () -> printfn "Checking %s at type %A\n" (Print.exp_to_string e) t);
       let e, t = check_term' g t f ty in
  
positive.code: (********************************************************************************************)
  let translate_typ (g:env) (t:term) : mlty = failwith ""
  
  (* instantiate s args:
          only handles fully applied types, 
          pre-condition: List.length (fst s) = List.length args
  *)
  let instantiate (s:mltyscheme) (args:list<mlty>) : mlty = Util.subst s args 
  
  (* erasable g f t:
         Ghost terms are erasable
         As are pure terms that return uninformative types, e.g., unit
  *)
  let erasable (g:env) (f:e_tag) (t:mlty) =
      f = E_GHOST || (f = E_PURE && erasableType g t)
  
  (* erase g t f:
          if t is an expression, replaces t with () if it is erasable
   *)
  let erase (g:env) e ty (f:e_tag) : (mlexpr * e_tag * mlty) =
      let e = if erasable g f ty
              then if type_leq g ty ml_unit_ty then ml_unit
  
negative.code:             else e in
      (e, f, ty)
  
  //maybe_coerce g e ty expect:
  //     Inserts an Obj.magic around e if ty </: expect
  let maybe_coerce (g:env) e ty (expect:mlty) : mlexpr  =
      let ty = eraseTypeDeep g ty in
      match type_leq_c g (Some e) ty expect with 
          | true, Some e' -> e'
          | _ -> with_ty expect <| MLE_Coerce (e, ty, expect)
  //         debug g (fun () -> printfn "\n (*needed to coerce expression \n %A \n of type \n %A \n to type \n %A *) \n" e tInferred tExpected);
        
  //////////////////////////////////////////////////////////////////////////////////////////////
  (********************************************************************************************)
  (* The main extraction of terms to ML expressions                                           *)
  (********************************************************************************************)
  //////////////////////////////////////////////////////////////////////////////////////////////
        
  //extract_pat g p
  //     Translates an F* pattern to an ML pattern
  //     The main work is erasing inaccessible (dot) patterns
  //     And turning F*'s curried pattern style to ML's fully applied ones                
  let extract_pat (g:env) p : (env * list<(mlpattern * option<mlexpr>)>) =
      let rec extract_one_pat (disjunctive_pat : bool) (imp : bool) g p : env * option<(mlpattern * list<mlexpr>)> = 
          match p.v with
            | Pat_disj _ -> failwith "Impossible"
   
  