diff options
Diffstat (limited to 'theories/Numbers/Integer/BigZ/ZMake.v')
| -rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 5927c2beab..83171388d9 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -17,7 +17,7 @@ Open Scope Z_scope. Module Type NType. - Parameter t : Set. + Parameter t : Type. Parameter zero : t. Parameter one : t. @@ -101,7 +101,7 @@ End NType. Module Make (N:NType). - Inductive t_ : Set := + Inductive t_ := | Pos : N.t -> t_ | Neg : N.t -> t_. |