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 3152478ab..7f6f05d11 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -176,7 +176,7 @@ let pred_case_ml_onebranch loc env sigma isrec indt (i,fj) = open Pp let mssg_may_need_inversion () = - [< 'sTR "This pattern-matching is not exhaustive.">] + str "This pattern-matching is not exhaustive." let mssg_this_case_cannot_occur () = "This pattern-matching is not exhaustive." |