diff options
| author | Pierre-Marie Pédrot | 2016-04-14 20:43:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-04 13:47:12 +0200 |
| commit | a2a8840a4fe1b3d6c6dbc27b5521b28bd319ff42 (patch) | |
| tree | 88108ed4457cb0b573e468752619a2939085dd1a /plugins | |
| parent | de4b9b68445d9f3e48da789404cbdfcd89214585 (diff) | |
More toplevel value representation sharing.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 1 |
1 files changed, 1 insertions, 0 deletions
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 |