aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
authorPierre Roux2020-09-03 13:27:00 +0200
committerPierre Roux2020-11-05 00:20:51 +0100
commitb6214bd4d5d3003e9b60411a717e84277feead24 (patch)
treecd0a04bbf1b9e43d21ec5944c4458d74797c5b09 /interp
parent3b766fd8859b692e3e93cf83bf87d393e32c572e (diff)
[string notation] Handle parameterized inductives and non inductives
Diffstat (limited to 'interp')
-rw-r--r--interp/notation.ml9
1 files changed, 5 insertions, 4 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index 1839e287d7..5f6fd62e5c 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1107,11 +1107,12 @@ let coqbyte_of_string ?loc byte s =
let p =
if Int.equal (String.length s) 1 then int_of_char s.[0]
else
- if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
- then int_of_string s
- else
+ let n =
+ if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
+ then int_of_string s else 256 in
+ if n < 256 then n else
user_err ?loc ~hdr:"coqbyte_of_string"
- (str "Expects a single character or a three-digits ascii code.") in
+ (str "Expects a single character or a three-digit ASCII code.") in
coqbyte_of_char_code byte p
let coqbyte_of_char byte c = coqbyte_of_char_code byte (Char.code c)