Merge pull request #98 from Nadrieril/update-charon

AeneasVerif · Dec 6, 2024 · 7164d1a · 7164d1a
2 parents ba9be28 + 063d4da
commit 7164d1a
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 7 deletions.
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -98,6 +98,7 @@
 
         inputsFrom = [
           self.packages.${system}.default
+          charon-ml
         ];
       };
     });

diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml
@@ -369,7 +369,9 @@ let rec typ_of_ty (env : env) (ty : Charon.Types.ty) : K.typ =
       (* Appears in some trait methods, so let's try to handle that. *)
       K.TBuf (typ_of_ty env t, false)
   | TTraitType _ -> failwith ("TODO: TraitTypes " ^ Charon.PrintTypes.ty_to_string env.format_env ty)
-  | TArrow (_, ts, t) -> Krml.Helpers.fold_arrow (List.map (typ_of_ty env) ts) (typ_of_ty env t)
+  | TArrow binder ->
+      let ts, t = binder.binder_value in
+      Krml.Helpers.fold_arrow (List.map (typ_of_ty env) ts) (typ_of_ty env t)
 
 and maybe_cg_array env t cg =
   match cg with
-Original file line number
+Diff line change
@@ Expand Up / @@ -98,6 +98,7 @@ @@
             inputsFrom = [
               self.packages.${system}.default
+              charon-ml
             ];
           };
         });
@@ Expand Down @@