From fe70dafd8302af50e76171307a78e7dedd26a9b3 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Tue, 2 Dec 2003 11:35:12 +0000
Subject: error messages adjustement

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5057 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/cc/ccproof.ml | 4 ++--
 contrib/cc/cctac.ml4  | 9 +++------
 2 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml
index 9bcdf56f21..8d5d2642b9 100644
--- a/contrib/cc/ccproof.ml
+++ b/contrib/cc/ccproof.ml
@@ -143,10 +143,10 @@ let cc_proof (axioms,m)=
 		    Prove (prf,axioms)
 		  else anomaly "wrong proof generated"
 	      else
-		errorlabstrm  "CC" (Pp.str "CC couldn't solve goal")
+		errorlabstrm  "Congruence" (Pp.str "I couldn't solve goal")
 	| None ->
 	    cc uf;
-	    errorlabstrm  "CC" (Pp.str "CC couldn't solve goal")
+	    errorlabstrm  "Congruence" (Pp.str "I couldn't solve goal")
     with UF.Discriminable (i,ci,j,cj,uf) ->
       let prf=build_proof uf (Refute(i,ci,j,cj)) in 
       let (t1,t2)=type_proof axioms prf in 
diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
index 2089d59974..61d04ef9a0 100644
--- a/contrib/cc/cctac.ml4
+++ b/contrib/cc/cctac.ml4
@@ -154,9 +154,9 @@ let rec proof_tac axioms=function
 		[tclTHEN (apply lemma2) (proof_tac axioms p2);
 		 reflexivity;
 		 fun gls ->
-		   errorlabstrm  "CC" 
+		   errorlabstrm  "Congruence" 
 		   (Pp.str 
-		      "CC doesn't know how to handle dependent equality.")]]
+		      "I don't know how to handle dependent equality")]]
 	     gls)
   | Inject (prf,cstr,nargs,argind)  as gprf->
       (fun gls ->
@@ -176,10 +176,7 @@ let rec proof_tac axioms=function
 	
 let cc_tactic gls=
   Library.check_required_library ["Coq";"Init";"Logic"];
-  let prb=
-    try make_prb gls with 
-	Not_an_eq ->
-	  errorlabstrm  "CC" (str "Goal is not an equality") in
+  let prb=make_prb gls in
     match (cc_proof prb) with
         Prove (p,axioms)-> proof_tac axioms p gls
       | Refute (t1,t2,p,axioms) ->
-- 
cgit v1.2.3