diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NDefOps.v')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NDefOps.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index 8df715af9d..ad7a9f3ae5 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -23,7 +23,7 @@ Include NStrongRecProp N. Definition if_zero (A : Type) (a b : A) (n : N.t) : A := recursion a (fun _ _ => b) n. -Implicit Arguments if_zero [A]. +Arguments if_zero [A] a b n. Instance if_zero_wd (A : Type) : Proper (Logic.eq ==> Logic.eq ==> N.eq ==> Logic.eq) (@if_zero A). |