From 7c8bafec648d5fa57f13e4260198c4e4f03da31f Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 17 Sep 2018 17:01:35 +0100
Subject: Coq: fix types in aarch64_extras undefined_vector and casts for
 arguments

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

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 1614d8de..45efa798 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1152,10 +1152,10 @@ let doc_exp, doc_let =
             let typ_from_fn = Env.expand_synonyms env typ_from_fn in
             (* TODO: more sophisticated check *)
             let () =
-              debug ctxt (lazy (" arg type found    " ^ string_of_typ (general_typ_of arg)));
+              debug ctxt (lazy (" arg type found    " ^ string_of_typ (typ_of arg)));
               debug ctxt (lazy (" arg type expected " ^ string_of_typ typ_from_fn))
             in
-            let typ_of_arg = Env.expand_synonyms env (general_typ_of arg) in
+            let typ_of_arg = Env.expand_synonyms env (typ_of arg) in
             let typ_of_arg = expand_range_type typ_of_arg in
             let typ_of_arg' = match typ_of_arg with Typ_aux (Typ_exist (_,_,t),_) -> t  | t -> t in
             let typ_from_fn' = match typ_from_fn with Typ_aux (Typ_exist (_,_,t),_) -> t  | t -> t in
-- 
cgit v1.2.3