From a2a8840a4fe1b3d6c6dbc27b5521b28bd319ff42 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 14 Apr 2016 20:43:57 +0200
Subject: More toplevel value representation sharing.

---
 plugins/funind/g_indfun.ml4 | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/funind')

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index e93c395e3d..0ba18f568a 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -65,6 +65,7 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
 
 
 ARGUMENT EXTEND fun_ind_using
+  TYPED AS constr_with_bindings option
   PRINTED BY pr_fun_ind_using_typed
   RAW_TYPED AS constr_with_bindings_opt
   RAW_PRINTED BY pr_fun_ind_using
-- 
cgit v1.2.3