diff options
Diffstat (limited to 'src/pretty_print_coq.ml')
| -rw-r--r-- | src/pretty_print_coq.ml | 13 |
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 = |