From 051e2a19f3268d272a0acd0425d2107ebea020c5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 7 Mar 2023 13:46:55 +0100
Subject: Reorganize the Lean tests and extract the Polonius tests to Lean

---
 compiler/Extract.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler')

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 *)
-- 
cgit v1.2.3