diff options
author | 2003-12-02 11:35:12 +0000 | |
---|---|---|
committer | 2003-12-02 11:35:12 +0000 | |
commit | fe70dafd8302af50e76171307a78e7dedd26a9b3 (patch) | |
tree | bd5c5d1c39192a2d3bd695bc87fd5c3f985bd533 /contrib/cc/cctac.ml4 | |
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/cctac.ml4')
-rw-r--r-- | contrib/cc/cctac.ml4 | 9 |
1 files changed, 3 insertions, 6 deletions
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) -> |