diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/cLexer.ml4 | 16 | ||||
| -rw-r--r-- | parsing/egramcoq.ml | 2 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 1 | ||||
| -rw-r--r-- | parsing/g_proofs.ml4 | 6 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 |
5 files changed, 15 insertions, 15 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 9c9189ffeb..f26398fa92 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -245,8 +245,8 @@ let check_ident str = loop_id true s | [< s >] -> match unlocated lookup_utf8 Ploc.dummy s with - | Utf8Token (Unicode.Letter, n) -> njunk n s; loop_id true s - | Utf8Token (Unicode.IdentPart, n) when intail -> + | Utf8Token (st, n) when not intail && Unicode.is_valid_ident_initial st -> njunk n s; loop_id true s + | Utf8Token (st, n) when intail && Unicode.is_valid_ident_trailing st -> njunk n s; loop_id true s | EmptyStream -> () @@ -311,9 +311,9 @@ let rec ident_tail loc len = parser ident_tail loc (store len c) s | [< s >] -> match lookup_utf8 loc s with - | Utf8Token ((Unicode.IdentPart | Unicode.Letter), n) -> + | Utf8Token (st, n) when Unicode.is_valid_ident_trailing st -> ident_tail loc (nstore n len s) s - | Utf8Token (Unicode.Unknown, n) -> + | Utf8Token (st, n) when Unicode.is_unknown st -> let id = get_buff len in let u = String.concat "" (List.map (String.make 1) (Stream.npeek n s)) in warn_unrecognized_unicode ~loc:!@loc (u,id); len @@ -539,7 +539,7 @@ let parse_after_dot loc c bp = (try find_keyword loc ("."^field) s with Not_found -> FIELD field) | [< s >] -> match lookup_utf8 loc s with - | Utf8Token (Unicode.Letter, n) -> + | Utf8Token (st, n) when Unicode.is_valid_ident_initial st -> let len = ident_tail loc (nstore n 0 s) s in let field = get_buff len in (try find_keyword loc ("."^field) s with Not_found -> FIELD field) @@ -553,7 +553,7 @@ let parse_after_qmark loc bp s = | None -> KEYWORD "?" | _ -> match lookup_utf8 loc s with - | Utf8Token (Unicode.Letter, _) -> LEFTQMARK + | Utf8Token (st, _) when Unicode.is_valid_ident_initial st -> LEFTQMARK | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars loc bp '?' s) @@ -618,13 +618,13 @@ let rec next_token loc = parser bp comment_stop bp; between_commands := new_between_commands; t | [< s >] -> match lookup_utf8 loc s with - | Utf8Token (Unicode.Letter, n) -> + | Utf8Token (st, n) when Unicode.is_valid_ident_initial st -> let len = ident_tail loc (nstore n 0 s) s in let id = get_buff len in let ep = Stream.count s in comment_stop bp; (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep - | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart | Unicode.Unknown), _) -> + | AsciiChar | Utf8Token _ -> let t = process_chars loc bp (Stream.next s) s in comment_stop bp; t | EmptyStream -> diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 870137ca11..d51b8b54e5 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -34,6 +34,7 @@ let default_levels = [200,Extend.RightA,false; 100,Extend.RightA,false; 99,Extend.RightA,true; + 90,Extend.RightA,true; 10,Extend.RightA,false; 9,Extend.RightA,false; 8,Extend.RightA,true; @@ -44,6 +45,7 @@ let default_pattern_levels = [200,Extend.RightA,true; 100,Extend.RightA,false; 99,Extend.RightA,true; + 90,Extend.RightA,true; 11,Extend.LeftA,false; 10,Extend.RightA,false; 1,Extend.LeftA,false; diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 4e8b98fcf2..844c040fdf 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -376,6 +376,7 @@ GEXTEND Gram | "100" RIGHTA [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CAst.make ~loc:!@loc @@ CPatOr (p::pl) ] | "99" RIGHTA [ ] + | "90" RIGHTA [ ] | "11" LEFTA [ p = pattern; "as"; id = ident -> CAst.make ~loc:!@loc @@ CPatAlias (p, id) ] diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 42b5bfa935..e2c87bbbf6 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -45,11 +45,9 @@ GEXTEND Gram | IDENT "Existential"; n = natural; c = constr_body -> VernacSolveExistential (n,c) | IDENT "Admitted" -> VernacEndProof Admitted - | IDENT "Qed" -> VernacEndProof (Proved (Opaque None,None)) - | IDENT "Qed"; IDENT "exporting"; l = LIST0 identref SEP "," -> - VernacEndProof (Proved (Opaque (Some l),None)) + | IDENT "Qed" -> VernacEndProof (Proved (Opaque,None)) | IDENT "Save"; id = identref -> - VernacEndProof (Proved (Opaque None, Some id)) + VernacEndProof (Proved (Opaque, Some id)) | IDENT "Defined" -> VernacEndProof (Proved (Transparent,None)) | IDENT "Defined"; id=identref -> VernacEndProof (Proved (Transparent,Some id)) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 4a59b85978..3e0b85b54a 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -131,7 +131,7 @@ let test_plural_form_types loc kwd = function let fresh_var env c = Namegen.next_ident_away (Id.of_string "pat") - (env @ Id.Set.elements (Topconstr.free_vars_of_constr_expr c)) + (List.fold_left (fun accu id -> Id.Set.add id accu) (Topconstr.free_vars_of_constr_expr c) env) let _ = Hook.set Constrexpr_ops.fresh_var_hook fresh_var @@ -1020,8 +1020,7 @@ GEXTEND Gram | IDENT "Term"; qid = smart_global -> LocateTerm qid | IDENT "File"; f = ne_string -> LocateFile f | IDENT "Library"; qid = global -> LocateLibrary qid - | IDENT "Module"; qid = global -> LocateModule qid - | IDENT "Ltac"; qid = global -> LocateTactic qid ] ] + | IDENT "Module"; qid = global -> LocateModule qid ] ] ; option_value: [ [ n = integer -> IntValue (Some n) |