diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 85c518019..18ad2ed3d 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -503,7 +503,7 @@ let set_used_pattern eqn = eqn.used := true let extract_rhs pb = match pb.mat with - | [] -> errorlabstrm "build_leaf" (msg_may_need_inversion()) + | [] -> user_err "build_leaf" (msg_may_need_inversion()) | eqn::_ -> set_used_pattern eqn; eqn.rhs |