diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 84a1cd550f..bd47badfe3 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1679,7 +1679,7 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs = let ty = evi.evar_concl in Typing.check env evd' body ty with e -> - pperrnl + msg_info (str "Ill-typed evar instantiation: " ++ fnl() ++ pr_evar_map evd' ++ fnl() ++ str "----> " ++ int ev ++ str " := " ++ |