From 0d1da885cc8ccfb9f995e5dcb0ed79e71e6020db Mon Sep 17 00:00:00 2001
From: Fabian Kunze
Date: Fri, 27 Nov 2020 20:58:19 +0100
Subject: Better primitive type support in custom string and numeral notations.
 - float and array values are now supported for printing and parsing in custom
 notations (and in notations defined using the ocaml API) - the three
 constants bound to the primitive float, int and array type are now allowed
 anywhere inside a term to print, to handle them similar to `real` type
 constructors - Grants #13484: String notations for primitive arrays - Fixes
 #13517: String notation printing fails with primitive integers inside lists

---
 engine/univGen.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'engine/univGen.ml')

diff --git a/engine/univGen.ml b/engine/univGen.ml
index 6f27ccb7dc..278ca6bf34 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -65,6 +65,11 @@ let fresh_constructor_instance env c =
   let u, ctx = fresh_global_instance env (GlobRef.ConstructRef c) in
   (c, u), ctx
 
+let fresh_array_instance env =
+  let auctx = CPrimitives.typ_univs CPrimitives.PT_array in
+  let u, ctx = fresh_instance_from auctx None in
+  u, ctx
+
 let fresh_global_instance ?loc ?names env gr =
   let u, ctx = fresh_global_instance ?loc ?names env gr in
   mkRef (gr, u), ctx
-- 
cgit v1.2.3