diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 49c0cd79c..ebf603111 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -289,8 +289,8 @@ GEXTEND Gram | n=INT -> CPrim (!@loc, Numeral (Bigint.of_string n)) | s=string -> CPrim (!@loc, String s) | "_" -> CHole (!@loc, None, IntroAnonymous, None) - | "?["; id=ident; "]" -> CHole (!@loc, None, IntroIdentifier id, None) - | "?["; id=pattern_ident; "]" -> CHole (!@loc, None, IntroFresh id, None) + | "?"; "["; id=ident; "]" -> CHole (!@loc, None, IntroIdentifier id, None) + | "?"; "["; id=pattern_ident; "]" -> CHole (!@loc, None, IntroFresh id, None) | id=pattern_ident; inst = evar_instance -> CEvar(!@loc,id,inst) ] ] ; inst: |