From f7992de2dc4ce0091197b9476779fc120a2fd9ec Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 27 Nov 2018 21:03:57 -0500
Subject: Factor out common code in numeral/string notations

As per https://github.com/coq/coq/pull/8965#issuecomment-441440779
---
 plugins/syntax/numeral.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/syntax/numeral.ml')

diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 10a0af0b8f..470deb4a60 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -125,7 +125,7 @@ let vernac_numeral_notation local ty f g scope opts =
       | None -> type_error_of g ty true
   in
   let o = { to_kind; to_ty; of_kind; of_ty;
-            num_ty = ty;
+            ty_name = ty;
             warning = opts }
   in
   (match opts, to_kind with
-- 
cgit v1.2.3