diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-07 12:24:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-12 13:37:07 +0200 |
| commit | c48ade3f0d6324872d292932e797ffd718ad57d9 (patch) | |
| tree | 8437ef0e8f366c0df9dcef5e0189cf075739e7c4 /plugins/firstorder/g_ground.ml4 | |
| parent | 519d2b0e5d6b53c2f2a02ee9b685088fd74be0f6 (diff) | |
A couple of fixes/improvements in -beautify, but backtracking on
change of printing format of forall (need more thinking).
Diffstat (limited to 'plugins/firstorder/g_ground.ml4')
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index c3ae05de6..10e2e1773 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -106,9 +106,9 @@ open Pp open Genarg open Ppconstr open Printer -let pr_firstorder_using_raw _ _ _ = prlist_with_sep pr_comma pr_reference -let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) -let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_comma pr_global +let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_reference l +let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l +let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l ARGUMENT EXTEND firstorder_using PRINTED BY pr_firstorder_using_typed |