diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-17 18:35:03 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-17 18:35:03 +0100 |
| commit | 00f82e4411ebbab16fcab99e6c563852a87507a3 (patch) | |
| tree | 46aa4acc7d1b9e8d6850c113e73cffbfc7dccb65 /tactics/autorewrite.ml | |
| parent | 6aa2cd90c3091ebe397d83e1d70caa6237b4b551 (diff) | |
Fixing bug #3796.
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 2be8020a7..d9a2da0e9 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -77,8 +77,8 @@ let find_matches bas pat = List.map snd res let print_rewrite_hintdb bas = - (str "Database " ++ str bas ++ (Pp.cut ()) ++ - prlist_with_sep Pp.cut + (str "Database " ++ str bas ++ fnl () ++ + prlist_with_sep fnl (fun h -> str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++ Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++ |