From fa0f378c91286d9127777a06b1dc557f695c22ae Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 14 Jul 2018 06:25:22 -0400 Subject: Fix numeral notation for a rebase on top of master Some of this code is cargo-culted or kludged to work. As I understand it, the situation is as follows: There are two sorts of use-cases that need to be supported: 1. A plugin registers an OCaml function as a numeral interpreter. In this case, the function registration must be synchronized with the document state, but the functions should not be marshelled / stored in the .vo. 2. A vernacular registers a Gallina function as a numeral interpreter. In this case, the registration must be synchronized, and the function should be marshelled / stored in the .vo. In case (1), we can compare functions by pointer equality, and we should be able to rely on globally unique keys, even across backtracking. In case (2), we cannot compare functions by pointer equality (because they must be regenerated on unmarshelling when `Require`ing a .vo file), and we also cannot rely on any sort of unique key being both unique and persistent across files. The solution we use here is that we ask clients to provide "unique" keys, and that clients tell us whether or not to overwrite existing registered functions, i.e., to tell us whether or not we should expect interpreter functions to be globally unique under pointer equality. For plugins, a simple string suffices, as long as the string does not clash between different plugins. In the case of vernacular-registered functions, use marshell a description of all of the data used to generate the function, and use that string as a unique key which is expected to persist across files. Because we cannot rely on function-pointer uniqueness here, we tell the interpretation-registration to allow overwriting. ---- Some of this code is response to comments on the PR ---- Some code is to fix an issue that bignums revealed: Both Int31 and bignums registered numeral notations in int31_scope. We now prepend a globally unique identifier when registering numeral notations from OCaml plugins. This is permissible because we don't store the uid information for such notations in .vo files (assuming I'm understanding the code correctly). --- doc/sphinx/user-extensions/syntax-extensions.rst | 160 ++++++++++++++++++----- interp/notation.ml | 37 +++--- interp/notation.mli | 8 +- plugins/syntax/g_numeral.ml4 | 80 +++++++----- test-suite/success/NumeralNotations.v | 55 ++++++++ theories/Numbers/AltBinNotations.v | 45 +++---- 6 files changed, 272 insertions(+), 113 deletions(-) create mode 100644 test-suite/success/NumeralNotations.v diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index e947fd891b..ca588acf29 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1379,42 +1379,130 @@ Numeral notations Starting with version 8.9, the following command allows the user to customize the way numeral literals are parsed and printed: -.. cmd:: Numeral Notation @ty @pa @pr : @scope. - -In the previous line, `ty` should be the name of an inductive type, -while `pa` and `pr` should be the names of two parsing and printing -functions. -The parsing function `pa` should have one of the following types: - - * :g:`Decimal.int -> ty` - * :g:`Decimal.int -> option ty` - * :g:`Decimal.uint -> ty` - * :g:`Decimal.uint -> option ty` - * :g:`Z -> ty` - * :g:`Z -> option ty` - -And the printing function `pr` should have one of the following types: - - * :g:`ty -> Decimal.int` - * :g:`ty -> option Decimal.int` - * :g:`ty -> Decimal.uint` - * :g:`ty -> option Decimal.uint` - * :g:`ty -> Z` - * :g:`ty -> option Z` - -.. cmdv:: Numeral Notation @ty @pa @pr : @scope (warning after @n). - -When a literal larger than `n` is parsed, a warning message about -possible stack overflow will be displayed. - -.. cmdv:: Numeral Notation @ty @pa @pr : @scope (abstract after @n). - -When a literal `m` larger than `n` is parsed, the result will be -:g:`(pa m)`, without reduction of this application to a normal form. -Here `m` will be a ``Decimal.int`` or ``Decimal.uint`` or ``Z``, -depending on the type of the parsing function `pa`. This allows a more -compact representation of literals in types such as ``nat``, and -limits parse failures due to stack overflow. +.. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope. + + In the previous line, :n:`@ident__1` should be the name of an + inductive type, while :n:`@ident__2` and :n:`@ident__3` should be + the names of the parsing and printing functions, respectively. The + parsing function :n:`@ident__2` should have one of the following + types: + + * :n:`Decimal.int -> @ident__1` + * :n:`Decimal.int -> option @ident__1` + * :n:`Decimal.uint -> @ident__1` + * :n:`Decimal.uint -> option @ident__1` + * :n:`Z -> @ident__1` + * :n:`Z -> option @ident__1` + + And the printing function :n:`@ident__3` should have one of the + following types: + + * :n:`@ident__1 -> Decimal.int` + * :n:`@ident__1 -> option Decimal.int` + * :n:`@ident__1 -> Decimal.uint` + * :n:`@ident__1 -> option Decimal.uint` + * :n:`@ident__1 -> Z` + * :n:`@ident__1 -> option Z` + + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). + + When a literal larger than :token:`num` is parsed, a warning + message about possible stack overflow, resulting from evaluating + :n:`@ident__2`, will be displayed. + + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (abstract after @num). + + When a literal :g:`m` larger than :token:`num` is parsed, the + result will be :n:`(@ident__2 m)`, without reduction of this + application to a normal form. Here :g:`m` will be a + :g:`Decimal.int` or :g:`Decimal.uint` or :g:`Z`, depending on the + type of the parsing function :n:`@ident__2`. This allows for a + more compact representation of literals in types such as :g:`nat`, + and limits parse failures due to stack overflow. Note that a + warning will be emitted when an integer larger than :token:`num` + is parsed. + + .. exn:: Cannot interpret this number as a value of type @type + + The numeral notation registered for :g:`ty` does not support the + given numeral. This error is given when the interpretation + function returns :g:`None`, or if the interpretation is registered + for only non-negative integers, and the given numeral is negative. + + .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + + The parsing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. + + .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the the types Decimal.uint or Z could be used{? (require BinNums first)}. + + The printing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. + + .. exn:: @type is not an inductive type + + Numeral notations can only be declared for inductive types with no + arguments. + + .. exn:: The inductive type @type cannot be used in numeral notations because support for polymorphic inductive types is not yet implemented. + + Numeral notations do not currently support polymorphic inductive + types. Ensure that all types involved in numeral notations are + declared with :g:`Unset Universe Polymorphism`, or with the + :g:`Monomorphic` attribute. + + .. exn:: The function @ident cannot be used in numeral notations because support for polymorphic printing and parsing functions is not yet implemented. + + Numeral notations do not currently support polymorphic functions + for printing and parsing. Ensure that both functions passed to + :cmd:`Numeral Notation` are defined with :g:`Unset Universe + Polymorphism`, or with the :g:`Monomorphic` attribute. + + .. exn:: Unexpected term while parsing a numeral notation + + Parsing functions must always return ground terms, made up of + applications of constructors and inductive types. Parsing + functions may not return terms containing axioms, bare + (co)fixpoints, lambdas, etc. + + .. exn:: Unexpected non-option term while parsing a numeral notation + + Parsing functions expected to return an :g:`option` must always + return a concrete :g:`Some` or :g:`None` when applied to a + concrete numeral expressed as a decimal. They may not return + opaque constants. + + .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). + + The type passed to :cmd:`Numeral Notation` must be a single + identifier. + + .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). + + Both functions passed to :cmd:`Numeral Notation` must be single + identifiers. + + .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). + + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(warning after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + + .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @ident__2. + + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(abstract after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + Typically, this indicates that the fully computed representation + of numerals can be so large that non-tail-recursive OCaml + functions run out of stack space when trying to walk them. + + For example + + .. coqtop:: all + + Check 90000. + .. _TacticNotation: diff --git a/interp/notation.ml b/interp/notation.ml index f60ddcf909..56d6acbdae 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -378,38 +378,39 @@ let prim_token_interp_infos = let prim_token_uninterp_infos = ref (Refmap.empty : (scope_name * prim_token_uid * bool) Refmap.t) -let hashtbl_check_and_set uid f h eq = +let hashtbl_check_and_set allow_overwrite uid f h eq = match Hashtbl.find h uid with | exception Not_found -> Hashtbl.add h uid f + | _ when allow_overwrite -> Hashtbl.add h uid f | g when eq f g -> () | _ -> user_err ~hdr:"prim_token_interpreter" (str "Unique identifier " ++ str uid ++ str " already used to register a numeral or string (un)interpreter.") -let register_gen_interpretation uid (interp, uninterp) = +let register_gen_interpretation allow_overwrite uid (interp, uninterp) = hashtbl_check_and_set - uid interp prim_token_interpreters InnerPrimToken.interp_eq; + allow_overwrite uid interp prim_token_interpreters InnerPrimToken.interp_eq; hashtbl_check_and_set - uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq + allow_overwrite uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq -let register_rawnumeral_interpretation uid (interp, uninterp) = - register_gen_interpretation uid +let register_rawnumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid (InnerPrimToken.RawNumInterp interp, InnerPrimToken.RawNumUninterp uninterp) -let register_bignumeral_interpretation uid (interp, uninterp) = - register_gen_interpretation uid +let register_bignumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid (InnerPrimToken.BigNumInterp interp, InnerPrimToken.BigNumUninterp uninterp) -let register_string_interpretation uid (interp, uninterp) = - register_gen_interpretation uid +let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp) type prim_token_infos = { pt_scope : scope_name; (** Concerned scope *) pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) pt_required : required_module; (** Module that should be loaded first *) - pt_refs : global_reference list; (** Entry points during uninterpretation *) + pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) pt_in_match : bool (** Is this prim token legal in match patterns ? *) } @@ -445,19 +446,25 @@ let enable_prim_token_interpretation infos = (the latter inside a [Mltop.declare_cache_obj]). *) +let fresh_string_of = + let count = ref 0 in + fun root -> count := !count+1; (string_of_int !count)^"_"^root + let declare_numeral_interpreter sc dir interp (patl,uninterp,b) = - register_bignumeral_interpretation sc (interp,uninterp); + let uid = fresh_string_of sc in + register_bignumeral_interpretation uid (interp,uninterp); enable_prim_token_interpretation { pt_scope = sc; - pt_uid = sc; + pt_uid = uid; pt_required = dir; pt_refs = List.map_filter glob_prim_constr_key patl; pt_in_match = b } let declare_string_interpreter sc dir interp (patl,uninterp,b) = - register_string_interpretation sc (interp,uninterp); + let uid = fresh_string_of sc in + register_string_interpretation uid (interp,uninterp); enable_prim_token_interpretation { pt_scope = sc; - pt_uid = sc; + pt_uid = uid; pt_required = dir; pt_refs = List.map_filter glob_prim_constr_key patl; pt_in_match = b } diff --git a/interp/notation.mli b/interp/notation.mli index 2545e494ef..1d01d75c82 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -91,19 +91,19 @@ type 'a prim_token_interpretation = 'a prim_token_interpreter * 'a prim_token_uninterpreter val register_rawnumeral_interpretation : - prim_token_uid -> rawnum prim_token_interpretation -> unit + ?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit val register_bignumeral_interpretation : - prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit + ?allow_overwrite:bool -> prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit val register_string_interpretation : - prim_token_uid -> string prim_token_interpretation -> unit + ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit type prim_token_infos = { pt_scope : scope_name; (** Concerned scope *) pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) pt_required : required_module; (** Module that should be loaded first *) - pt_refs : global_reference list; (** Entry points during uninterpretation *) + pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) pt_in_match : bool (** Is this prim token legal in match patterns ? *) } diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 index caba4db4fc..19a15fd1df 100644 --- a/plugins/syntax/g_numeral.ml4 +++ b/plugins/syntax/g_numeral.ml4 @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* strbrk "Stack overflow or segmentation fault happens when " ++ - strbrk "working with large numbers in " ++ pr_reference ty ++ + strbrk "working with large numbers in " ++ pr_qualid ty ++ strbrk " (threshold may vary depending" ++ strbrk " on your system limits and on the command executed).") @@ -64,11 +65,11 @@ let warn_abstract_large_num = (fun (ty,f) -> let (sigma, env) = Pfedit.get_current_context () in strbrk "To avoid stack overflow, large numbers in " ++ - pr_reference ty ++ strbrk " are interpreted as applications of " ++ + pr_qualid ty ++ strbrk " are interpreted as applications of " ++ Printer.pr_constr_env env sigma f ++ strbrk ".") (** Comparing two raw numbers (base 10, big-endian, non-negative). - A bit nasty, but not critical : only used to decide when a + A bit nasty, but not critical: only used to decide when a number is considered as large (see warnings above). *) exception Comp of int @@ -233,18 +234,24 @@ let rec glob_of_constr ?loc c = match Constr.kind c with | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None)) | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None)) | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None)) - | _ -> CErrors.anomaly (str "Numeral.interp: unexpected constr") + | _ -> let (sigma, env) = Pfedit.get_current_context () in + CErrors.user_err ?loc + (str "Unexpected term while parsing a numeral notation:" ++ fnl () ++ + Printer.pr_constr_env env sigma c) let no_such_number ?loc ty = CErrors.user_err ?loc (str "Cannot interpret this number as a value of type " ++ - pr_reference ty) + pr_qualid ty) let interp_option ty ?loc c = match Constr.kind c with | App (_Some, [| _; c |]) -> glob_of_constr ?loc c | App (_None, [| _ |]) -> no_such_number ?loc ty - | x -> CErrors.anomaly (str "Numeral.interp: option expected") + | x -> let (sigma, env) = Pfedit.get_current_context () in + CErrors.user_err ?loc + (str "Unexpected non-option term while parsing a numeral notation:" ++ fnl () ++ + Printer.pr_constr_env env sigma c) let uninterp_option c = match Constr.kind c with @@ -276,7 +283,7 @@ type numeral_notation_obj = to_ty : constr; of_kind : conversion_kind; of_ty : constr; - num_ty : Libnames.reference; (* for warnings / error messages *) + num_ty : Libnames.qualid; (* for warnings / error messages *) warning : numnot_option } let interp o ?loc n = @@ -322,7 +329,7 @@ let uninterp o (Glob_term.AnyGlobConstr n) = let load_numeral_notation _ (_, (uid,opts)) = Notation.register_rawnumeral_interpretation - uid (interp opts, uninterp opts) + ~allow_overwrite:true uid (interp opts, uninterp opts) let cache_numeral_notation x = load_numeral_notation 1 x @@ -355,7 +362,7 @@ let unsafe_locate_ind q = let locate_ind q = try unsafe_locate_ind q - with Not_found -> Nametab.error_global_not_found (CAst.make q) + with Not_found -> Nametab.error_global_not_found q let locate_z () = try @@ -367,35 +374,33 @@ let locate_int () = { uint = locate_ind q_uint; int = locate_ind q_int } -let locate_globref r = - let q = qualid_of_reference r in - try Nametab.locate CAst.(q.v) +let locate_globref q = + try Nametab.locate q with Not_found -> Nametab.error_global_not_found q -let locate_constant r = - let q = qualid_of_reference r in - try Nametab.locate_constant CAst.(q.v) +let locate_constant q = + try Nametab.locate_constant q with Not_found -> Nametab.error_global_not_found q let has_type f ty = let (sigma, env) = Pfedit.get_current_context () in - let c = mkCastC (mkRefC f, CastConv ty) in + let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in try let _ = Constrintern.interp_constr env sigma c in true with Pretype_errors.PretypeError _ -> false let type_error_to f ty loadZ = CErrors.user_err - (pr_reference f ++ str " should go from Decimal.int to " ++ - pr_reference ty ++ str " or (option " ++ pr_reference ty ++ str ")." ++ - fnl () ++ str "Instead of int, the types uint or Z could be used" ++ - (if loadZ then str " (load Z first)." else str ".")) + (pr_qualid f ++ str " should go from Decimal.int to " ++ + pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ + fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ + (if loadZ then str " (require BinNums first)." else str ".")) let type_error_of g ty loadZ = CErrors.user_err - (pr_reference g ++ str " should go from " ++ pr_reference ty ++ - str " to Decimal.int or (option int)." ++ fnl () ++ - str "Instead of int, the types uint or Z could be used" ++ - (if loadZ then str " (load Z first)." else str ".")) + (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ + str " to Decimal.int or (option Decimal.int)." ++ fnl () ++ + str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ + (if loadZ then str " (require BinNums first)." else str ".")) let vernac_numeral_notation ty f g scope opts = let int_ty = locate_int () in @@ -405,7 +410,7 @@ let vernac_numeral_notation ty f g scope opts = let of_ty = mkConst (locate_constant g) in let cty = mkRefC ty in let app x y = mkAppC (x,[y]) in - let cref q = mkRefC (CAst.make (Qualid q)) in + let cref q = mkRefC q in let arrow x y = mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) in @@ -420,17 +425,20 @@ let vernac_numeral_notation ty f g scope opts = get_constructors ind | IndRef _ -> CErrors.user_err - (str "The inductive type " ++ pr_reference ty ++ - str " cannot be polymorphic here for the moment") + (str "The inductive type " ++ pr_qualid ty ++ + str " cannot be used in numeral notations because" ++ + str " support for polymorphic inductive types is not yet implemented") | ConstRef _ | ConstructRef _ | VarRef _ -> CErrors.user_err - (pr_reference ty ++ str " is not an inductive type") + (pr_qualid ty ++ str " is not an inductive type") in (* Check the type of f *) let to_kind = if Global.is_polymorphic (Nametab.global f) then CErrors.user_err - (pr_reference f ++ str " cannot be polymorphic for the moment") + (str "The function " ++ pr_qualid f ++ str " cannot be used" ++ + str " in numeral notations because support for polymorphic" ++ + str " printing and parsing functions is not yet implemented.") else if has_type f (arrow cint cty) then Int int_ty, Direct else if has_type f (arrow cint (opt cty)) then Int int_ty, Option else if has_type f (arrow cuint cty) then UInt int_ty.uint, Direct @@ -447,7 +455,7 @@ let vernac_numeral_notation ty f g scope opts = let of_kind = if Global.is_polymorphic (Nametab.global g) then CErrors.user_err - (pr_reference g ++ str " cannot be polymorphic for the moment") + (pr_qualid g ++ str " cannot be polymorphic for the moment") else if has_type g (arrow cty cint) then Int int_ty, Direct else if has_type g (arrow cty (opt cint)) then Int int_ty, Option else if has_type g (arrow cty cuint) then UInt int_ty.uint, Direct diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v new file mode 100644 index 0000000000..a06327c5e6 --- /dev/null +++ b/test-suite/success/NumeralNotations.v @@ -0,0 +1,55 @@ + +(* Test that we fail, rather than raising anomalies, on opaque terms during interpretation *) + +(* https://github.com/coq/coq/pull/8064#discussion_r202497516 *) +Module Test1. + Axiom hold : forall {A B C}, A -> B -> C. + Definition opaque3 (x : Decimal.int) : Decimal.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end). + Numeral Notation Decimal.int opaque3 opaque3 : opaque_scope. + Delimit Scope opaque_scope with opaque. + Fail Check 1%opaque. +End Test1. + +(* https://github.com/coq/coq/pull/8064#discussion_r202497990 *) +Module Test2. + Axiom opaque4 : option Decimal.int. + Definition opaque6 (x : Decimal.int) : option Decimal.int := opaque4. + Numeral Notation Decimal.int opaque6 opaque6 : opaque_scope. + Delimit Scope opaque_scope with opaque. + Open Scope opaque_scope. + Fail Check 1%opaque. +End Test2. + +Module Test3. + Inductive silly := SILLY (v : Decimal.uint) (f : forall A, A -> A). + Definition to_silly (v : Decimal.uint) := SILLY v (fun _ x => x). + Definition of_silly (v : silly) := match v with SILLY v _ => v end. + Numeral Notation silly to_silly of_silly : silly_scope. + Delimit Scope silly_scope with silly. + Fail Check 1%silly. +End Test3. + + +Module Test4. + Polymorphic Inductive punit := ptt. + Polymorphic Definition pto_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end. + Polymorphic Definition pof_punit (v : punit) : Decimal.uint := Nat.to_uint 0. + Definition to_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end. + Definition of_punit (v : punit) : Decimal.uint := Nat.to_uint 0. + Polymorphic Definition pto_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end. + Polymorphic Definition pof_unit (v : unit) : Decimal.uint := Nat.to_uint 0. + Definition to_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end. + Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0. + Fail Numeral Notation punit to_punit of_punit : pto. + Fail Numeral Notation punit pto_punit of_punit : ppo. + Fail Numeral Notation punit to_punit pof_punit : ptp. + Fail Numeral Notation punit pto_punit pof_punit : ppp. + Numeral Notation unit to_unit of_unit : uto. + Delimit Scope uto with uto. + Check let v := 0%uto in v : unit. + Fail Check 1%uto. + Fail Check (-1)%uto. + Fail Numeral Notation unit pto_unit of_unit : upo. + Fail Numeral Notation unit to_unit pof_unit : utp. + Fail Numeral Notation unit pto_unit pof_unit : upp. +End Test4. diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v index 595934ad89..c7e3999691 100644 --- a/theories/Numbers/AltBinNotations.v +++ b/theories/Numbers/AltBinNotations.v @@ -1,34 +1,35 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(*