From fab70aaf2947ff1369757355fbf11437c6db35ff Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Sun, 30 Jun 2024 15:07:02 +0200
Subject: implement syntax for non-dependent function and pair types

---
 src/pretty/Pretty.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'src/pretty/Pretty.ml')

diff --git a/src/pretty/Pretty.ml b/src/pretty/Pretty.ml
index ba78881..8b7ad1a 100644
--- a/src/pretty/Pretty.ml
+++ b/src/pretty/Pretty.ml
@@ -67,8 +67,9 @@ struct
        pp scrut pp_local_name motive_var (bind motive_var pp) motive pp true_case pp false_case
     ) fmt
 
-  and pp_arg fmt (name, tp) =
-    Fmt.pf fmt "(@[%a@] : @[%a@])" pp_local_name name pp tp
+  and pp_arg fmt (name, tp) = match name with
+    | Some name -> (delimited @@ fun fmt (name, tp) -> Fmt.pf fmt "(@[%s@] : @[%a@])" name pp tp) fmt (name, tp)
+    | None -> pp fmt tp
 
   (* TODO: improve indentation *)
   and pp fmt = function
-- 
cgit 1.4.1