diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-02 11:35:12 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-02 11:35:12 +0000 |
| commit | fe70dafd8302af50e76171307a78e7dedd26a9b3 (patch) | |
| tree | bd5c5d1c39192a2d3bd695bc87fd5c3f985bd533 /contrib/cc | |
| parent | 49091a7b9dd029e42caa22152449185f1c5a2039 (diff) | |
error messages adjustement
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5057 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/cc')
| -rw-r--r-- | contrib/cc/ccproof.ml | 4 | ||||
| -rw-r--r-- | 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 9bcdf56f2..8d5d2642b 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 2089d5997..61d04ef9a 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) -> |