blob: ea3907ef8aa8ca26000d7ddf5e0f3fb6ed27317c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
(* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *)
Inductive unit11 := tt11.
Declare Scope unit11_scope.
Delimit Scope unit11_scope with unit11.
Goal True.
evar (to_uint : unit11 -> Decimal.uint).
evar (of_uint : Decimal.uint -> unit11).
Fail Numeral Notation unit11 of_uint to_uint : uint11_scope.
exact I.
Unshelve.
all: solve [ constructor ].
Qed.
|
