diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-06 22:45:05 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-06 22:45:05 +0200 |
| commit | 5a3d4adc631f5b5d3dc4585b7b28ea18b6faf633 (patch) | |
| tree | 299bdd3c6068f121ca243d8602addcd27d690fd2 /backend/PrintCminor.ml | |
| parent | c420bc8d3b87d71c38209b5ab8bca22875466362 (diff) | |
| parent | c6356cdc5f567a317afcb99cb004354cf7dcce0f (diff) | |
| download | compcert-kvx-5a3d4adc631f5b5d3dc4585b7b28ea18b6faf633.tar.gz compcert-kvx-5a3d4adc631f5b5d3dc4585b7b28ea18b6faf633.zip | |
Merge remote-tracking branch 'origin/mppa-work' into mppa-expect
Diffstat (limited to 'backend/PrintCminor.ml')
| -rw-r--r-- | backend/PrintCminor.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 8c255a65..c9a6d399 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -16,7 +16,7 @@ (** Pretty-printer for Cminor *) open Format -open !Camlcoq +open! Camlcoq open Integers open AST open PrintAST @@ -193,9 +193,7 @@ let print_sig p sg = List.iter (fun t -> fprintf p "%s ->@ " (name_of_type t)) sg.sig_args; - match sg.sig_res with - | None -> fprintf p "void" - | Some ty -> fprintf p "%s" (name_of_type ty) + fprintf p "%s" (name_of_rettype sg.sig_res) let rec just_skips s = match s with |