From b73f6d13b4bf2291f71616abdb046e2ca657d868 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 15 Aug 2018 13:59:16 +0100
Subject: Get RISC-V on Coq into reasonable state to show - Fill in Coq
 builtins for more of the RISC-V prelude - Update Barriers - More general
 autocast - Temporary sub_nat definition (until the backend handles nat
 better) - Patch to bring results into a reasonable state - Use Let rather
 than Definition for non-dependent top-level values

---
 src/pretty_print_coq.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index d5aa7151..fb53db96 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1954,13 +1954,12 @@ let doc_val pat exp =
   in
   let idpp = doc_id id in
   let basepp =
-    group (string "Definition" ^^ space ^^ idpp ^^ typpp ^^ space ^^ coloneq ^/^
-             doc_exp_lem ctxt false exp ^^ dot) ^^ hardline
+    idpp ^^ typpp ^^ space ^^ coloneq ^/^ doc_exp_lem ctxt false exp ^^ dot
   in
   match opt_unpack with
-  | None -> basepp ^^ hardline
+  | None -> group (string "Let" ^^ space ^^ basepp) ^^ hardline
   | Some (orig_id, hyp_id) ->
-     basepp ^^
+     group (string "Definition" ^^ space ^^ basepp) ^^ hardline ^^
        group (separate space [string "Let"; doc_id orig_id; coloneq; string "projT1"; idpp; dot]) ^^ hardline ^^ hardline
 
 let rec doc_def unimplemented def =
-- 
cgit v1.2.3