From 2814ee0f33045842b7ebfb5f36629062e1ad511d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 14 Apr 2006 18:22:55 +0000
Subject: Pas fier

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8717 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4ad85af9a8..0874d56e5d 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -793,7 +793,7 @@ let prepare_unif_pb typ cs =
   let typ' =
     if noccur_between_without_evar 1 n typ then lift (-n) typ
     else (* TODO4-1 *)
-      error "Inference of annotation not yet implemented in this case" in
+      error "Unable to infer return clause of this pattern-matching problem" in
   let args = extended_rel_list (-n) cs.cs_args in
   let ci = applist (mkConstruct cs.cs_cstr, cs.cs_params@args) in
 
-- 
cgit v1.2.3