diff options
| -rw-r--r-- | grammar/q_util.mlp | 8 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.ml | 23 |
2 files changed, 24 insertions, 7 deletions
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 536ee7ca5..c2d767396 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -94,10 +94,14 @@ let coincide s pat off = done; !break +let check_separator sep = + if sep <> "" then failwith "Separator is only for arguments with suffix _list_sep." + let rec parse_user_entry s sep = let l = String.length s in if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then let entry = parse_user_entry (String.sub s 3 (l-8)) "" in + check_separator sep; Ulist1 entry else if l > 12 && coincide s "ne_" 0 && coincide s "_list_sep" (l-9) then @@ -105,16 +109,20 @@ let rec parse_user_entry s sep = Ulist1sep (entry, sep) else if l > 5 && coincide s "_list" (l-5) then let entry = parse_user_entry (String.sub s 0 (l-5)) "" in + check_separator sep; Ulist0 entry else if l > 9 && coincide s "_list_sep" (l-9) then let entry = parse_user_entry (String.sub s 0 (l-9)) "" in Ulist0sep (entry, sep) else if l > 4 && coincide s "_opt" (l-4) then let entry = parse_user_entry (String.sub s 0 (l-4)) "" in + check_separator sep; Uopt entry else if l = 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then let n = Char.code s.[6] - 48 in + check_separator sep; Uentryl ("tactic", n) else let s = match s with "hyp" -> "var" | _ -> s in + check_separator sep; Uentry s diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 0bf6e3d15..ee84be541 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -63,28 +63,37 @@ let get_separator = function | None -> user_err Pp.(str "Missing separator.") | Some sep -> sep -let rec parse_user_entry s sep = +let check_separator ?loc = function +| None -> () +| Some _ -> user_err ?loc (str "Separator is only for arguments with suffix _list_sep.") + +let rec parse_user_entry ?loc s sep = let l = String.length s in if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then - let entry = parse_user_entry (String.sub s 3 (l-8)) None in + let entry = parse_user_entry ?loc (String.sub s 3 (l-8)) None in + check_separator ?loc sep; Ulist1 entry else if l > 12 && coincide s "ne_" 0 && coincide s "_list_sep" (l-9) then - let entry = parse_user_entry (String.sub s 3 (l-12)) None in + let entry = parse_user_entry ?loc (String.sub s 3 (l-12)) None in Ulist1sep (entry, get_separator sep) else if l > 5 && coincide s "_list" (l-5) then - let entry = parse_user_entry (String.sub s 0 (l-5)) None in + let entry = parse_user_entry ?loc (String.sub s 0 (l-5)) None in + check_separator ?loc sep; Ulist0 entry else if l > 9 && coincide s "_list_sep" (l-9) then - let entry = parse_user_entry (String.sub s 0 (l-9)) None in + let entry = parse_user_entry ?loc (String.sub s 0 (l-9)) None in Ulist0sep (entry, get_separator sep) else if l > 4 && coincide s "_opt" (l-4) then - let entry = parse_user_entry (String.sub s 0 (l-4)) None in + let entry = parse_user_entry ?loc (String.sub s 0 (l-4)) None in + check_separator ?loc sep; Uopt entry else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then let n = Char.code s.[6] - 48 in + check_separator ?loc sep; Uentryl ("tactic", n) else + let _ = check_separator ?loc sep in Uentry s let interp_entry_name interp symb = @@ -203,7 +212,7 @@ let register_tactic_notation_entry name entry = let interp_prod_item = function | TacTerm s -> TacTerm s | TacNonTerm (loc, ((nt, sep), ido)) -> - let symbol = parse_user_entry nt sep in + let symbol = parse_user_entry ?loc nt sep in let interp s = function | None -> if String.Map.mem s !entry_names then String.Map.find s !entry_names |