diff options
| author | Pierre Roux | 2021-02-09 18:23:11 +0100 |
|---|---|---|
| committer | Pierre Roux | 2021-02-27 12:07:39 +0100 |
| commit | c02bbaeb9c6c9cbc4a7f2dc47876a94fdd33aa5e (patch) | |
| tree | f2288e6e102d9711b2e327cbd2502ecd109ae15d /interp/notation.mli | |
| parent | 3915bc904fc16060c25baaf7d5626e3587ad2891 (diff) | |
Remove decimal-only number notations
This was deprecated in 8.12
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 3 |
1 files changed, 0 insertions, 3 deletions
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 |