diff options
Diffstat (limited to 'parsing/g_ltac.ml4')
| -rw-r--r-- | parsing/g_ltac.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index f5309fa39..5c74f4ef6 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -230,7 +230,7 @@ GEXTEND Gram | n = integer -> Integer n | id = METAIDENT -> MetaIdArg (loc,id) | "?" -> ConstrMayEval (ConstrTerm (CHole loc)) - | "?"; n = natural -> ConstrMayEval (ConstrTerm (CMeta (loc,n))) + | "?"; n = natural -> ConstrMayEval (ConstrTerm (CPatVar (loc,(false,Pattern.patvar_of_int n)))) | "'"; c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ] ; |