diff options
| author | ppedrot | 2012-06-01 20:08:33 +0000 |
|---|---|---|
| committer | ppedrot | 2012-06-01 20:08:33 +0000 |
| commit | a92a0d051b987ba996905ccd4ce7ee3a5feb41c1 (patch) | |
| tree | ec5246ac1cfc741dc30c33fe6551216dfdef6a54 /pretyping | |
| parent | 80b91aa1e83097efd006cfed5f57e4826a1ab0c8 (diff) | |
More cleaning
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15414 85f007b7-540e-0410-9357-904b9bb8a0f7
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 " := " ++ |