diff options
Diffstat (limited to 'theories/Numbers/Natural/SpecViaZ')
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index a0ad7643d..2c7884ac4 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -445,7 +445,7 @@ Qed. Definition recursion (A : Type) (a : A) (f : NN.t -> A -> A) (n : NN.t) := Nrect (fun _ => A) a (fun n a => f (NN.of_N n) a) (NN.to_N n). -Implicit Arguments recursion [A]. +Arguments recursion [A] a f n. Instance recursion_wd (A : Type) (Aeq : relation A) : Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A). |