diff options
| -rw-r--r-- | parsing/g_tactic.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index b1f68d0701..98e3d6ead8 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -254,7 +254,7 @@ GEXTEND Gram | IDENT "Induction"; n = pure_numarg -> <:ast< (Induction $n) >> | IDENT "NewInduction"; c=ident_or_constrarg -> <:ast<(NewInduction $c)>> | IDENT "NewInduction"; n = pure_numarg -> <:ast< (NewInduction $n) >> - | IDENT "Double"; IDENT "Induction"; i = numarg; j = numarg -> + | IDENT "Double"; IDENT "Induction"; i = pure_numarg; j = pure_numarg -> <:ast< (DoubleInd $i $j) >> | IDENT "Trivial" -> <:ast<(Trivial)>> | IDENT "Trivial"; "with"; lid = ne_identarg_list -> |