diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-21 11:09:18 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-21 11:09:18 +0000 |
| commit | 1766059a85a44893839ee52e0840f26638da02bf (patch) | |
| tree | 24a771a1288b6104683abd7efd3a385c035e8203 /contrib/cc | |
| parent | d7fcf7e0ef2fcee500a1436b8b9d5c0b8a5c8530 (diff) | |
Messages de idtac et fail peuvent maintenant être des listes de string, int et variables ltac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7909 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/cc')
| -rw-r--r-- | contrib/cc/cctac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |