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.

1 files changed, 2 insertions, 3 deletions

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
             | _ ->