diff options
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 70450295be..3d0691b18d 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -335,6 +335,8 @@ let explain_hole_kind env = function str ") of this term" | GoalEvar -> str "an existential variable" + | ImpossibleCase -> + str "the type of an impossible pattern-matching clause" let explain_not_clean env ev t k = let env = make_all_name_different env in |