From 446931aa3eff319d37b8a98fdf1e877dde4514dc Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 22 May 2019 17:55:07 +0100
Subject: Coq: replace inferrable integer arguments with _ at more types
 Previously we only checked at atom, now use destruct_atom_nexp to pick up
 implicit too.

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

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 445ac1cb..bb1ba201 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1700,9 +1700,8 @@ let doc_exp, doc_let =
               let ekids = Env.get_typ_vars env in
               KidSet.for_all (fun kid -> KBindings.mem kid ekids) (nexp_frees n)
             in
-            match typ_of_arg, typ_from_fn with
-            | Typ_aux (Typ_app (Id_aux (Id "atom",_),[A_aux (A_nexp n1,_)]),_),
-              Typ_aux (Typ_app (Id_aux (Id "atom",_),[A_aux (A_nexp n2,_)]),_)
+            match destruct_atom_nexp env typ_of_arg, destruct_atom_nexp env typ_from_fn with
+            | Some n1, Some n2
                  when vars_in_env n2 && not (similar_nexps ctxt env n1 n2) ->
                underscore
             | _ ->
-- 
cgit v1.2.3