From 209738abe5f77ea8f04f7cff6bccb133c4cccb33 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 6 Oct 2000 16:06:07 +0000 Subject: Mise en page de Print Hint git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@670 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/auto.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index 953f2f74a..aeb0cfb59 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -475,7 +475,7 @@ let fmt_hint_list_for_head c = [<'sTR "No hint declared for :"; pr_ref_label c >] else hOV 0 - [< 'sTR"For "; pr_ref_label c; 'sTR" -> "; + [< 'sTR"For "; pr_ref_label c; 'sTR" -> "; 'fNL; prlist (fun (name,db,hintlist) -> [< 'sTR " In the database "; 'sTR name; 'sTR " :"; 'fNL; fmt_hint_list hintlist >]) @@ -535,7 +535,7 @@ let print_hint_db db = Hint_db.iter (fun head hintlist -> mSG (hOV 0 - [< 'sTR "For "; pr_ref_label head; 'sTR " -> "; + [< 'sTR "For "; pr_ref_label head; 'sTR " -> "; fmt_hint_list hintlist; 'fNL >])) db -- cgit v1.2.3