diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Extract.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 0e9a53df..63d41d9a 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -973,7 +973,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter) if !backend = FStar && fields = [] then ( F.pp_print_space fmt (); F.pp_print_string fmt (unit_name ())) - else if (not is_rec) || !backend = FStar then ( + else if (not is_rec) || !backend <> Coq then ( F.pp_print_space fmt (); (* If Coq: print the constructor name *) (* TODO: remove superfluous test not is_rec below *) |