aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-04-20 17:24:58 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-04 13:47:12 +0200
commit729d838838d8df06395726477817620e2ae998bc (patch)
tree50986942f010f2a9281aa19dd715bd1f67dd921e /plugins
parent4740e82e4af6d38e9cc55dfe1a05db87f73bf1e6 (diff)
Interpretation function can return any untyped value.
Diffstat (limited to 'plugins')
-rw-r--r--plugins/firstorder/g_ground.ml41
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 587d10d1c..b04c4a50c 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -122,6 +122,7 @@ let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma
let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
ARGUMENT EXTEND firstorder_using
+ TYPED AS reference_list
PRINTED BY pr_firstorder_using_typed
RAW_TYPED AS reference_list
RAW_PRINTED BY pr_firstorder_using_raw