summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/Translate.ml5
-rw-r--r--flake.lock6
2 files changed, 7 insertions, 4 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 222b3c57..72a98c3d 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -798,7 +798,10 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
(* Translate *)
export_functions_group pure_funs
| GlobalGroup id -> export_global id
- | TraitDeclGroup id ->
+ | TraitDeclGroup (RecGroup _ids) ->
+ craise_opt_meta __FILE__ __LINE__ None
+ "Mutually recursive trait declarations are not supported"
+ | TraitDeclGroup (NonRecGroup id) ->
(* TODO: update to extract groups *)
if config.extract_trait_decls && config.extract_transparent then (
export_trait_decl_group id;
diff --git a/flake.lock b/flake.lock
index fd118ae3..b9178971 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
"rust-overlay": "rust-overlay"
},
"locked": {
- "lastModified": 1714668124,
- "narHash": "sha256-66QkLemEGCWI+XnGYOA666XLMdrV5PU6Oew2B1fil+4=",
+ "lastModified": 1715000450,
+ "narHash": "sha256-N7VGgAwoMeSEYblcKzo7TZWv6upuJdknrnZO1ZSwJWQ=",
"owner": "aeneasverif",
"repo": "charon",
- "rev": "9d08aa01e4c2b94c24c7c79e47191d626a1a03b4",
+ "rev": "f8fab8d2f4f279f973057d0f7f58c2fd59146e30",
"type": "github"
},
"original": {