From 91d62c6e73cd67236848c3efa85f85ae152d0d4e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 8 Feb 2024 09:42:00 +0100
Subject: Update following changes in Charon

---
 compiler/Extract.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'compiler/Extract.ml')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 46f6a1ca..a93ed6e4 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -326,11 +326,8 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
           extract_adt_cons ctx fmt inside adt_cons_id qualif.generics args
       | Proj proj ->
           extract_field_projector ctx fmt inside app proj qualif.generics args
-      | TraitConst (trait_ref, generics, const_name) ->
-          let use_brackets = generics <> empty_generic_args in
-          if use_brackets then F.pp_print_string fmt "(";
+      | TraitConst (trait_ref, const_name) ->
           extract_trait_ref ctx fmt TypeDeclId.Set.empty false trait_ref;
-          extract_generic_args ctx fmt TypeDeclId.Set.empty generics;
           let name =
             ctx_get_trait_const trait_ref.trait_decl_ref.trait_decl_id
               const_name ctx
@@ -338,7 +335,6 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
           let add_brackets (s : string) =
             if !backend = Coq then "(" ^ s ^ ")" else s
           in
-          if use_brackets then F.pp_print_string fmt ")";
           F.pp_print_string fmt ("." ^ add_brackets name))
   | _ ->
       (* "Regular" expression *)
-- 
cgit v1.2.3