aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/g_ground.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/g_ground.ml4')
-rw-r--r--plugins/firstorder/g_ground.ml46
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