From eec5145a5c6575d04b5ab442597fb52913daed29 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 4 Feb 2017 14:56:04 +0100 Subject: Applying same convention as in Definition for printing type in a let in. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Also adding spaces around ":=" and ":" when printed as "(x : t := c)". Example: Check fun y => let x : True := I in fun z => z+y=0. (* λ (y : nat) (x : True := I) (z : nat), z + y = 0 : nat → nat → Prop *) --- printing/ppconstr.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'printing/ppconstr.ml') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 0013d49a1..f36c8c153 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -363,8 +363,9 @@ let tag_var = tag Tag.variable | CLocalAssum (nal,k,t) -> pr_binder true pr_c (nal,k,t) | CLocalDef (na,c,topt) -> - surround (pr_lname na ++ str":=" ++ cut() ++ pr_c c ++ - pr_opt_no_spc (fun t -> cut () ++ str ":" ++ pr_c t) topt) + surround (pr_lname na ++ + pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++ + str" :=" ++ spc() ++ pr_c c) | CLocalPattern (loc,p,tyo) -> let p = pr_patt lsimplepatt p in match tyo with @@ -598,9 +599,9 @@ let tag_var = tag Tag.variable | CLetIn (_,x,a,t,b) -> return ( hv 0 ( - hov 2 (keyword "let" ++ spc () ++ pr_lname x ++ str " :=" - ++ pr spc ltop a ++ spc () - ++ pr_opt_no_spc (fun t -> str ":" ++ ws 1 ++ pr mt ltop t ++ spc ()) t + hov 2 (keyword "let" ++ spc () ++ pr_lname x + ++ pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr mt ltop t) t + ++ str " :=" ++ pr spc ltop a ++ spc () ++ keyword "in") ++ pr spc ltop b), lletin -- cgit v1.2.3