From fa682c18c8ffc5fa7224d9e9d0e0dd94250ada57 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Aug 2023 00:28:10 +0200
Subject: Make a minor formatting modification for Lean

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

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index c5f7df92..17355dfd 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -855,7 +855,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
       (* Always open the Primitives namespace *)
       Printf.fprintf out "open Primitives\n";
       (* If we are inside the namespace: declare it, otherwise: open it *)
-      if fi.in_namespace then Printf.fprintf out "namespace %s\n" fi.namespace
+      if fi.in_namespace then Printf.fprintf out "\nnamespace %s\n" fi.namespace
       else Printf.fprintf out "open %s\n" fi.namespace
   | HOL4 ->
       Printf.fprintf out "open primitivesLib divDefLib\n";
-- 
cgit v1.2.3