diff options
| author | Alasdair | 2020-09-29 16:23:40 +0100 |
|---|---|---|
| committer | Alasdair | 2020-09-29 16:32:24 +0100 |
| commit | 7441db19749fb7fb9383b6361dfbd99547e53486 (patch) | |
| tree | 779f90dbe139bce648540d517be84b156d92319e /src/pretty_print_coq.ml | |
| parent | 6dbd0facf0962d869d0c3957f668b035a4a6605c (diff) | |
Refactor: Change AST type from a union to a struct
Diffstat (limited to 'src/pretty_print_coq.ml')
| -rw-r--r-- | src/pretty_print_coq.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index cc5cd4da..7f28fac8 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -3232,7 +3232,6 @@ let doc_val pat exp = group (separate space [string "Hint Unfold"; idpp; colon; string "sail."]) ^^ hardline let rec doc_def unimplemented generic_eq_types def = - (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *) match def with | DEF_spec v_spec -> doc_val_spec unimplemented v_spec | DEF_fixity _ -> empty @@ -3281,7 +3280,7 @@ let find_unimplemented defs = in List.fold_left adjust_def IdSet.empty defs -let pp_defs_coq (types_file,types_modules) (defs_file,defs_modules) (Defs defs) top_line suppress_MR_M = +let pp_ast_coq (types_file,types_modules) (defs_file,defs_modules) { defs; _ } top_line suppress_MR_M = try (* let regtypes = find_regtypes d in *) let state_ids = |