diff options
| author | Guillaume Boisseau | 2024-06-28 10:58:44 +0200 |
|---|---|---|
| committer | GitHub | 2024-06-28 10:58:44 +0200 |
| commit | 5590dc87a5426cbcb32a2387701d179e107a9792 (patch) | |
| tree | 57f062f6243ae878b3fbc0df5abb9b7a938cb7f7 /compiler/Pure.ml | |
| parent | 2e9d264566d32a9ee2a12d005851434cd8390975 (diff) | |
| parent | 617941a779baab199aa69bf2e8578a1ee7877289 (diff) | |
Merge pull request #272 from Nadrieril/remove-llbc_name
Diffstat (limited to 'compiler/Pure.ml')
| -rw-r--r-- | compiler/Pure.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/compiler/Pure.ml b/compiler/Pure.ml index d273546a..2754eaac 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -397,8 +397,6 @@ type predicates = { trait_type_constraints : trait_type_constraint list } type type_decl = { def_id : TypeDeclId.id; - llbc_name : llbc_name; - (** The original name coming from the LLBC declaration *) name : string; (** We use the name only for printing purposes (for debugging): the name used at extraction time will be derived from the @@ -1106,7 +1104,6 @@ type fun_decl = { *) loop_id : LoopId.id option; (** [Some] if this definition was generated for a loop *) - llbc_name : llbc_name; (** The original LLBC name. *) name : string; (** We use the name only for printing purposes (for debugging): the name used at extraction time will be derived from the @@ -1122,7 +1119,6 @@ type global_decl = { def_id : GlobalDeclId.id; span : span; item_meta : T.item_meta; - llbc_name : llbc_name; (** The original LLBC name. *) name : string; (** We use the name only for printing purposes (for debugging): the name used at extraction time will be derived from the @@ -1140,7 +1136,6 @@ type global_decl = { type trait_decl = { def_id : trait_decl_id; - llbc_name : llbc_name; name : string; item_meta : T.item_meta; generics : generic_params; @@ -1162,7 +1157,6 @@ type trait_decl = { type trait_impl = { def_id : trait_impl_id; - llbc_name : llbc_name; name : string; item_meta : T.item_meta; impl_trait : trait_decl_ref; |