aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--grammar/q_util.mlp8
-rw-r--r--plugins/ltac/tacentries.ml23
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