diff --git a/lib/Monomorphization.ml b/lib/Monomorphization.ml index b3bd1175..d5aa81f3 100644 --- a/lib/Monomorphization.ml +++ b/lib/Monomorphization.ml @@ -379,8 +379,8 @@ module Gen = struct let doc = let open PPrint in let open PrintAst in - separate_map underscore print_typ ts ^^ underscore ^^ - separate_map underscore print_expr cgs + separate_map underscore print_typ ts ^^ + (if cgs = [] then empty else underscore ^^ separate_map underscore print_expr cgs) in fst lid, snd lid ^ KPrint.bsprintf "__%a" PrintCommon.pdoc doc diff --git a/test/.hints/Rust1.fst.hints b/test/.hints/Rust1.fst.hints index 9fcb1a1f..d8f31467 100644 --- a/test/.hints/Rust1.fst.hints +++ b/test/.hints/Rust1.fst.hints @@ -20,7 +20,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "5bb324f2cfa11752ab6a4b007bdd2ac9" + "d8d782168aeb290839dc8db99793893b" ], [ "Rust1.two", @@ -41,7 +41,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "19af3f16124ed6131ebd118a1645f272" + "b977b9a8e679010dd7db6093c2b24d8a" ], [ "Rust1.zero", @@ -62,7 +62,7 @@ "typing_FStar.Monotonic.HyperStack.get_hmap" ], 0, - "d085467eb557cb757d2b85c57ebf2d84" + "f86c73e1af7e81dadb23c04c7c9f2a29" ], [ "Rust1.doesnt_work", @@ -150,7 +150,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "91f166bd89ddce81d6c4629fdda8bac7" + "d6ead5099b52df6e78f527a435081340" ], [ "Rust1.does_work", @@ -238,7 +238,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "fe0681b3f23222e6fe18d1c809712105" + "15b8216a10f04a5bca9b51bdab9afc07" ], [ "Rust1.fully_static", @@ -327,7 +327,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "28f783251277dfe18bc75dccb61fd8a4" + "fc56150d57736c34acb5641ad70c2f88" ], [ "Rust1.main", @@ -416,7 +416,7 @@ "typing_LowStar.Monotonic.Buffer.loc_buffer" ], 0, - "68a280be773e96f4eb3f61ae14d6c637" + "7a928ff143175d99fb65b5f56469a5e5" ] ] ] \ No newline at end of file