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/evd.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 59eea97ce9..706e51d4b3 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -983,6 +983,9 @@ let fresh_inductive_instance ?loc ?(rigid=univ_flexible) env evd i =
 let fresh_constructor_instance ?loc ?(rigid=univ_flexible) env evd c =
   with_context_set ?loc rigid evd (UnivGen.fresh_constructor_instance env c)
 
+let fresh_array_instance ?loc ?(rigid=univ_flexible) env evd =
+  with_context_set ?loc rigid evd (UnivGen.fresh_array_instance env)
+
 let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
   with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr)
 
-- 
cgit v1.2.3