diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-28 07:33:41 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-28 07:33:41 +0000 |
| commit | 9a431a1b43dead6d692c942986a25f0f8986465a (patch) | |
| tree | 5d11bfeee35709817dc664168fa3be1dc42f5cb1 /toplevel | |
| parent | c43f9128237ac16fa0d7741744e3944ca72e7475 (diff) | |
Repairing r16205: errors raised by check_evar_instance were no longer
trapped by solve_simple_eqn.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16257 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 61830603b..9680a0046 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -183,9 +183,12 @@ let explain_unification_error env sigma p1 p2 = function | MetaOccurInBody evk -> spc () ++ str "(instance for " ++ quote (pr_existential_key evk) ++ strbrk " refers to a metavariable - please report your example)" - | InstanceNotSameType evk -> + | InstanceNotSameType (evk,env,t,u) -> spc () ++ str "(unable to find a well-typed instantiation for " ++ - quote (pr_existential_key evk) ++ str ")" + quote (pr_existential_key evk) ++ str ":" ++ spc () ++ + str "cannot unify" ++ + pr_lconstr_env env t ++ spc () ++ str "and" ++ spc () ++ + pr_lconstr_env env u ++ str ")" | UnifUnivInconsistency -> spc () ++ str "(Universe inconsistency)" |