From e1fc55c055f7636dea9c05819aefae61d7224698 Mon Sep 17 00:00:00 2001
From: jforest
Date: Thu, 14 Sep 2006 12:52:11 +0000
Subject: mise en conformite des messages d'erreur de Function avec la doc.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9136 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/funind/indfun.ml |  4 ++--
 contrib/funind/invfun.ml | 13 ++++++++++---
 2 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index cfaa2d4d7f..9a8d52eb7c 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -266,7 +266,7 @@ let derive_inversion fix_names =
 	)
     with e -> 
       msg_warning 
-	(str "Cannot define correction of function and graph" ++ 
+	(str "Cannot built inversion information" ++ 
 	   if do_observe () then Cerrors.explain_exn e else mt ())
   with _ -> ()
 
@@ -518,7 +518,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 		     (None:Vernacexpr.decl_notation)
 		 | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> 
 		     error 
-		       ("Cannot use mutual definition with well-founded recursion")
+		       ("Cannot use mutual definition with well-founded recursion or measure")
 	      ) 
 	      (List.combine fixpoint_exprl recdefs)
 	  in
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index a4c379bae0..40c90f5a1b 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -975,10 +975,17 @@ let invfun qhyp f g =
 			 functional_inversion kn hid  f2 f_correct g
 		       with
 			 | Failure "" -> 
-			     errorlabstrm "" (Ppconstr.pr_id hid ++ str " must contain at leat one function")
+			     errorlabstrm "" (str "Hypothesis" ++ Ppconstr.pr_id hid ++ str " must contain at leat one Function")
 			 | Failure "out_some"  ->  
-			     error "Cannot use equivalence with graph for any side of equality"
-			 | Not_found -> error "No graph found for any side of equality" 
+			     if do_observe () 
+			     then
+			       error "Cannot use equivalence with graph for any side of the equality"
+			     else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+			 | Not_found -> 
+			     if do_observe () 
+			     then
+			       error "No graph found for any side of equality" 
+			     else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
 		   end
 	       | _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ")
 	  )
-- 
cgit v1.2.3