diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-06 16:06:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-06 16:06:07 +0000 |
| commit | 209738abe5f77ea8f04f7cff6bccb133c4cccb33 (patch) | |
| tree | 9a89f41e3900ce3f55fbc3dba6547450c14acd7c /tactics | |
| parent | 3245946afceac0336d31b9e272484874c6b89471 (diff) | |
Mise en page de Print Hint
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@670 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |