From 1766059a85a44893839ee52e0840f26638da02bf Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 21 Jan 2006 11:09:18 +0000 Subject: Messages de idtac et fail peuvent maintenant être des listes de string, int et variables ltac MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7909 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/cc/cctac.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'contrib/cc') diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml index a3e1902c0..e6ce0ad66 100644 --- a/contrib/cc/cctac.ml +++ b/contrib/cc/cctac.ml @@ -287,7 +287,7 @@ let cc_tactic additionnal_terms gls= let _ = debug Pp.msgnl (Pp.str "Computation completed.") in let uf=forest state in match sol with - None -> tclFAIL 0 "congruence failed" gls + None -> tclFAIL 0 (str "congruence failed") gls | Some reason -> debug Pp.msgnl (Pp.str "Goal solved, generating proof ..."); match reason with @@ -318,7 +318,7 @@ let cc_tactic additionnal_terms gls= end); Pp.msgnl (Pp.str " replacing metavariables by arbitrary terms."); - tclFAIL 0 "Incomplete" gls + tclFAIL 0 (str "Incomplete") gls | Contradiction dis -> let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in let ta=term uf dis.lhs and tb=term uf dis.rhs in -- cgit v1.2.3