summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2023-03-07 13:46:55 +0100
committerSon HO2023-06-04 21:44:33 +0200
commit051e2a19f3268d272a0acd0425d2107ebea020c5 (patch)
tree2ad36d00054ac891e48cb35c4dc1940433c5e707 /compiler
parent463cbb90c93ac2e825048d685c254431b99c4d96 (diff)
Reorganize the Lean tests and extract the Polonius tests to Lean
Diffstat (limited to '')
-rw-r--r--compiler/Extract.ml2
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 *)