diff options
| author | pes20 | 2019-08-22 08:42:16 +0100 |
|---|---|---|
| committer | pes20 | 2019-08-22 08:42:16 +0100 |
| commit | c7975a53294d6c7ca9cfce7931489ba3f2bc35c8 (patch) | |
| tree | 833c7e0d9cf1077932f84a0b3ac453b7af7f9a98 /src/pretty_print_coq.ml | |
| parent | 7821c136a4e83cf25367852d2bffdebf850bd70a (diff) | |
additional option to tweak Coq output to support user-defined monad:
-coq_alt_modules2 <filename> provide additional alternative modules to open only in main (non-_types) Coq output, and suppress default definitions of MR and M monads
Diffstat (limited to 'src/pretty_print_coq.ml')
| -rw-r--r-- | src/pretty_print_coq.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 3d50d48c..bbee8fdc 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -3149,7 +3149,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 = +let pp_defs_coq (types_file,types_modules) (defs_file,defs_modules) (Defs defs) top_line suppress_MR_M = try (* let regtypes = find_regtypes d in *) let state_ids = @@ -3189,10 +3189,10 @@ try separate empty (List.map doc_def statedefs); hardline; hardline; register_refs; hardline; - concat [ + (if suppress_MR_M then empty else concat [ string ("Definition MR a r := monadR register_value a r " ^ exc_typ ^ "."); hardline; string ("Definition M a := monad register_value a " ^ exc_typ ^ "."); hardline - ] + ]) ]); (print defs_file) (concat |