diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 629c20177..0d431ea93 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -422,7 +422,7 @@ GEXTEND Gram let c = match n with | Some n -> let l = list_tabulate (fun _ -> (CHole (loc),None)) n in - CApp (loc,c,l) + CApp (loc,(false,c),l) | None -> c in VernacNotation (false,c,Some("'"^id^"'",[]),None,None) | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" -> |