diff options
author | 2006-01-19 22:34:29 +0000 | |
---|---|---|
committer | 2006-01-19 22:34:29 +0000 | |
commit | 0c0eeea26aafd36301d4b5592225e34153ff955f (patch) | |
tree | 1d839759bc9efc76ab3a0e09a5b52aa3039fffc7 /pretyping/cases.ml | |
parent | 46af7a39c66bc711fb32a5ce4fed4ab4f218d6af (diff) | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Merge commit 'upstream/8.0pl3'
Diffstat (limited to 'pretyping/cases.ml')
-rw-r--r-- | pretyping/cases.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 378eee30..4aff508f 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml,v 1.111.2.4 2004/12/09 20:07:01 herbelin Exp $ *) +(* $Id: cases.ml,v 1.111.2.5 2005/04/29 16:31:03 herbelin Exp $ *) open Util open Names @@ -171,10 +171,7 @@ let pred_case_ml env sigma isrec (IndType (indf,realargs)) (i,ft) = open Pp let mssg_may_need_inversion () = - str "This pattern-matching is not exhaustive." - -let mssg_this_case_cannot_occur () = - "This pattern-matching is not exhaustive." + str "Found a matching with no clauses on a term unknown to have an empty inductive type" (* Utils *) let make_anonymous_patvars = |