diff options
| -rw-r--r-- | tactics/extraargs.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 3fbd27c605..914e7671f8 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -58,7 +58,7 @@ ARGUMENT EXTEND raw GLOB_TYPED AS rawconstr_and_expr GLOB_PRINTED BY pr_gen - [ constr(c) ] -> [ c ] + [ lconstr(c) ] -> [ c ] END |