diff options
Diffstat (limited to 'theories/Arith')
| -rw-r--r-- | theories/Arith/Wf_nat.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index b55451233..05be5e1a3 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -258,6 +258,4 @@ Qed. Unset Implicit Arguments. -Notation iter_nat := @nat_iter (only parsing). -Notation iter_nat_plus := @nat_iter_plus (only parsing). -Notation iter_nat_invariant := @nat_iter_invariant (only parsing). +Notation iter_nat n A f x := (nat_rect (fun _ => A) x (fun _ => f) n) (only parsing). |