give better error message on forbidden identifiers

src/export/rawdk.ml

@@ -198,6 +198,7 @@ let command : p_command pp = fun ppf ({elt; pos} as c) ->
   | P_query q -> query ppf q
   | P_require(None,ps) ->
       List.iter (fun {elt;_} -> out ppf "#REQUIRE %a@." Dk.mident elt) ps
+  | P_symbol{p_sym_prf=Some(_,{elt=P_proof_abort;_}); _} -> ()
   | P_symbol{p_sym_mod; p_sym_kw=_; p_sym_nam=n; p_sym_arg; p_sym_typ;
              p_sym_trm; p_sym_prf=None; p_sym_def=_;} ->
       let ms = partition_modifiers p_sym_mod in
@@ -231,11 +232,11 @@ let command : p_command pp = fun ppf ({elt; pos} as c) ->
   | P_builtin _
   | P_unif_rule _
   | P_coercion _
-    -> () (*FIXME?*)
-  | P_inductive _
+    -> ()
+  | P_inductive _ (*FIXME*)
   | P_open _
   | P_require_as _
-  | P_notation _ (* FIXME: accept quantifier notations *)
+  | P_notation _
   | P_opaque _
   | P_require(Some _,_)
   | P_symbol{p_sym_prf=Some _; _}

src/parsing/lpLexer.ml

@@ -28,7 +28,7 @@ let fail : lexbuf -> string -> 'a = fun lb msg ->
 
 (* raises an unrecoverable lexing error; do not use in the parser *)
 let invalid_character : lexbuf -> 'a = fun lb ->
-  fail lb "Invalid character"
+  fail lb "Invalid character."
 
 (** Tokens. *)
 type token =
@@ -156,7 +156,6 @@ let float = [%sedlex.regexp? int, '.', nat]
 let oneline_comment = [%sedlex.regexp? "//", Star (Compl ('\n' | '\r'))]
 let string = [%sedlex.regexp? '"', Star (Compl '"'), '"']
 let positive_digit = [%sedlex.regexp? '1' .. '9']
-let strict_nat = [%sedlex.regexp? '0' | positive_digit, Star digit]
 
 (** Identifiers.
 
@@ -344,7 +343,10 @@ let rec token ~allow_rocq_syntax lb =
   | id -> UID(Utf8.lexeme lb)
   | '@', id -> UID_EXPL(remove_first lb)
   | '?', nat -> UID_META(int_of_string(remove_first lb))
-  | '$', nat -> fail lb "Forbidden pattern variable name"
+  | '?', '0', nat -> fail lb "Forbidden metavariable name."
+  | '?', id -> fail lb "Forbidden metavariable name."
+  | '$', nat -> fail lb "Forbidden pattern variable name."
+  | '$', '0', nat -> fail lb "Forbidden pattern variable name."
   | '$', id -> UID_PATT(remove_first lb)
 
   | id, '.' -> qid false [remove_last lb] lb
@@ -359,9 +361,9 @@ let token :
    lexbuf -> token * Lexing.position * Lexing.position =
   fun ~allow_rocq_syntax lb ->
     try Sedlexing.with_tokenizer (token ~allow_rocq_syntax) lb () with
-    | MalFormed -> fail lb "Not Utf8 encoded file"
+    | MalFormed -> fail lb "Not Utf8 encoded file."
     | InvalidCodepoint k ->
-       fail lb ("Invalid Utf8 code point " ^ string_of_int k)
+       fail lb ("Invalid Utf8 code point \""^string_of_int k^"\".")
 
 let dummy_token = (EOF, Lexing.dummy_pos, Lexing.dummy_pos)