Remove some assumed types and add more support for builtin definitions

1 files changed, 4 insertions, 4 deletions

diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index a982af30..2553127a 100644
--- a/compiler/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
@@ -5,13 +5,13 @@ let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
     fun_sig =
   match fun_id with
   | Regular id -> (FunDeclId.Map.find id fun_decls).signature
-  | Assumed aid -> Assumed.get_assumed_sig aid
+  | Assumed aid -> Assumed.get_assumed_fun_sig aid
 
 let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
     Names.fun_name =
   match fun_id with
   | Regular id -> (FunDeclId.Map.find id fun_decls).name
-  | Assumed aid -> Assumed.get_assumed_name aid
+  | Assumed aid -> Assumed.get_assumed_fun_name aid
 
 (** Return the opaque declarations found in the crate.
 
@@ -22,7 +22,7 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
  *)
 let crate_get_opaque_decls (k : crate) (filter_assumed : bool) :
     T.type_decl list * fun_decl list =
-  let open ExtractAssumed in
+  let open ExtractBuiltin in
   let is_opaque_fun (d : fun_decl) : bool =
     let sname = name_to_simple_name d.name in
     d.body = None
@@ -30,7 +30,7 @@ let crate_get_opaque_decls (k : crate) (filter_assumed : bool) :
        (which don't have a body but must not be considered as opaque) *)
     && (match d.kind with TraitMethodDecl _ -> false | _ -> true)
     && ((not filter_assumed)
-       || not (SimpleNameMap.mem sname assumed_globals_map))
+       || not (SimpleNameMap.mem sname builtin_globals_map))
   in
   let is_opaque_type (d : T.type_decl) : bool = d.kind = T.Opaque in
   (* Note that by checking the function bodies we also the globals *)