From c02bbaeb9c6c9cbc4a7f2dc47876a94fdd33aa5e Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 9 Feb 2021 18:23:11 +0100
Subject: Remove decimal-only number notations

This was deprecated in 8.12
---
 interp/notation.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'interp/notation.mli')

diff --git a/interp/notation.mli b/interp/notation.mli
index 77f245ae77..195f2a4416 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -146,9 +146,6 @@ type target_kind =
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
   | Int63 of pos_neg_int63_ty (* Coq.Numbers.Cyclic.Int63.PrimInt63.pos_neg_int63 *)
   | Number of number_ty (* Coq.Init.Number.number + uint + int *)
-  | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *)
-  | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *)
-  | Decimal of number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
 
 type string_target_kind =
   | ListByte
-- 
cgit v1.2.3