diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NDefOps.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NStrongRec.v | 2 |
2 files changed, 2 insertions, 2 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). diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index 039eefdf59..607746d59e 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -190,7 +190,7 @@ Qed. End FixPoint. End StrongRecursion. -Implicit Arguments strong_rec [A]. +Arguments strong_rec [A] a f n. End NStrongRecProp. |