From b6214bd4d5d3003e9b60411a717e84277feead24 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:27:00 +0200
Subject: [string notation] Handle parameterized inductives and non inductives

---
 interp/notation.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'interp')

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)
-- 
cgit v1.2.3