summaryrefslogtreecommitdiff
path: root/compiler/SymbolicToPure.ml
diff options
context:
space:
mode:
authorSon Ho2023-11-06 18:11:24 +0100
committerSon Ho2023-11-06 18:11:24 +0100
commit4ba7d73fa3bfbf9ef41b2d9d5595f28fb67b8e47 (patch)
tree45bfd5a0b82f7494c273b1a263787eba39b0d515 /compiler/SymbolicToPure.ml
parentdc0032f6ce3b837ba2f431bbb5c9a92c625f629f (diff)
Update following some changes in Charon
Diffstat (limited to '')
-rw-r--r--compiler/SymbolicToPure.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index c629a96f..46aa3b83 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3096,6 +3096,7 @@ let translate_trait_decl (type_infos : TA.type_infos)
name;
generics;
preds;
+ parent_clauses;
consts;
types;
required_methods;
@@ -3105,6 +3106,7 @@ let translate_trait_decl (type_infos : TA.type_infos)
in
let generics = translate_generic_params generics in
let preds = translate_predicates preds in
+ let parent_clauses = List.map translate_trait_clause parent_clauses in
let consts =
List.map
(fun (name, (ty, id)) -> (name, (translate_fwd_ty type_infos ty, id)))
@@ -3123,6 +3125,7 @@ let translate_trait_decl (type_infos : TA.type_infos)
name;
generics;
preds;
+ parent_clauses;
consts;
types;
required_methods;