diff options
| author | Pierre Roux | 2020-10-28 10:32:58 +0100 |
|---|---|---|
| committer | Pierre Roux | 2020-11-05 00:20:53 +0100 |
| commit | 36ac26532028bfc6f84e4dfc849b51f42a3d8286 (patch) | |
| tree | 9a8057cf3171c7b8fcf1ca2aa452cddb3d14e0fc /interp/notation.ml | |
| parent | e3593abd322acb59c512b5f2f776091546b38887 (diff) | |
Rename Dec and HexDec to Decimal and Hexadecimal
As noted by Hugo Herbelin, Dec is rather used for "decidable".
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 10e620b58a..a0321aaf82 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -836,8 +836,8 @@ let coqnumber_of_rawnum inds c n = mkApp (mkConstruct (ind, 2), [|i; f; e|]) (* (D|Hexad)ecimalExp *) let mkDecHex ind c n = match c with - | CDec -> mkApp (mkConstruct (ind, 1), [|n|]) (* (UInt|Int|)Dec *) - | CHex -> mkApp (mkConstruct (ind, 2), [|n|]) (* (UInt|Int|)Hex *) + | CDec -> mkApp (mkConstruct (ind, 1), [|n|]) (* (UInt|Int|)Decimal *) + | CHex -> mkApp (mkConstruct (ind, 2), [|n|]) (* (UInt|Int|)Hexadecimal *) exception NonDecimal @@ -912,8 +912,8 @@ let rawnum_of_coqnumber cl c = let destDecHex c = match Constr.kind c with | App (c,[|c'|]) -> (match Constr.kind c with - | Construct ((_,1), _) (* (UInt|Int|)Dec *) -> CDec, c' - | Construct ((_,2), _) (* (UInt|Int|)Hex *) -> CHex, c' + | Construct ((_,1), _) (* (UInt|Int|)Decimal *) -> CDec, c' + | Construct ((_,2), _) (* (UInt|Int|)Hexadecimal *) -> CHex, c' | _ -> raise NotAValidPrimToken) | _ -> raise NotAValidPrimToken |