diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 8b90824fd..7ab9488de 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -82,7 +82,7 @@ let pr_intro_as_pat prc _ _ pat = | None -> mt () -ARGUMENT EXTEND with_names TYPED AS intro_pattern_opt PRINTED BY pr_intro_as_pat +ARGUMENT EXTEND with_names TYPED AS simple_intropattern_opt PRINTED BY pr_intro_as_pat | [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] | [] ->[ None ] END |