Coq: fix false existential problem

1 files changed, 7 insertions, 6 deletions

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 7a31465d..32a560ea 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1023,16 +1023,17 @@ let doc_exp_lem, doc_let_lem =
             (* Decide whether to unpack an existential result, pack one, or cast.
                To do this we compare the expected type stored in the checked expression
                with the inferred type. *)
-            let ret_typ_inst =
-              match infer_exp env (strip_exp full_exp) with
-              | typed_exp -> typ_of typed_exp
+            let inst =
+              match instantiation_of_without_type full_exp with
+              | x -> x
               (* Not all function applications can be inferred, so try falling back to the
                  type inferred when we know the target type.
                  TODO: there are probably some edge cases where this won't pick up a need
                  to cast. *)
-              | exception _ ->
-                 let inst = instantiation_of full_exp in
-                 let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in
+              | exception _ -> instantiation_of full_exp
+            in
+            let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in
+            let ret_typ_inst =
                  subst_unifiers inst ret_typ
             in
             let unpack,build_ex,autocast =