diff options
| author | Brian Campbell | 2018-08-15 13:59:16 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-08-15 13:59:16 +0100 |
| commit | b73f6d13b4bf2291f71616abdb046e2ca657d868 (patch) | |
| tree | e999f8ccde5f510a9c004197b7fa142c346d9982 /src | |
| parent | 39fea17bac77535c9cff47cd6657a308e391ac8a (diff) | |
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
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 7 |
1 files changed, 3 insertions, 4 deletions
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 = |