diff options
| author | ppedrot | 2012-06-01 18:03:06 +0000 |
|---|---|---|
| committer | ppedrot | 2012-06-01 18:03:06 +0000 |
| commit | cf7660a3a8932ee593a376e8ec7ec251896a72e3 (patch) | |
| tree | 5f3fd167f5dd704bf5482d236624aa8ef8bf6707 /plugins/cc/cctac.ml | |
| parent | 35e4ac349af4fabbc5658b5cba632f98ec04da3f (diff) | |
Getting rid of Pp.msgnl and Pp.message.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/cc/cctac.ml')
| -rw-r--r-- | plugins/cc/cctac.ml | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 7940009c6e..204af93d56 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -378,16 +378,16 @@ let build_term_to_complete uf meta pac = let cc_tactic depth additionnal_terms gls= Coqlib.check_required_library ["Coq";"Init";"Logic"]; - let _ = debug Pp.msgnl (Pp.str "Reading subgoal ...") in + let _ = debug (Pp.str "Reading subgoal ...") in let state = make_prb gls depth additionnal_terms in - let _ = debug Pp.msgnl (Pp.str "Problem built, solving ...") in + let _ = debug (Pp.str "Problem built, solving ...") in let sol = execute true state in - let _ = debug Pp.msgnl (Pp.str "Computation completed.") in + let _ = debug (Pp.str "Computation completed.") in let uf=forest state in match sol with None -> tclFAIL 0 (str "congruence failed") gls | Some reason -> - debug Pp.msgnl (Pp.str "Goal solved, generating proof ..."); + debug (Pp.str "Goal solved, generating proof ..."); match reason with Discrimination (i,ipac,j,jpac) -> let p=build_proof uf (`Discr (i,ipac,j,jpac)) in @@ -400,10 +400,10 @@ let cc_tactic depth additionnal_terms gls= List.map (build_term_to_complete uf newmeta) (epsilons uf) in - Pp.msgnl + Pp.msg_info (Pp.str "Goal is solvable by congruence but \ some arguments are missing."); - Pp.msgnl + Pp.msg_info (Pp.str " Try " ++ hov 8 begin @@ -413,9 +413,8 @@ let cc_tactic depth additionnal_terms gls= (Termops.print_constr_env (pf_env gls)) terms_to_complete ++ str ")\"," - end); - Pp.msgnl - (Pp.str " replacing metavariables by arbitrary terms."); + end ++ + Pp.str " replacing metavariables by arbitrary terms."); tclFAIL 0 (str "Incomplete") gls | Contradiction dis -> let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in |