diff options
Diffstat (limited to 'theories/Arith/Max.v')
| -rw-r--r-- | theories/Arith/Max.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index c7e81505c..62250fc33 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -16,7 +16,7 @@ Implicit Types m n p : nat. (** * Maximum of two natural numbers *) -Fixpoint max n m {struct n} : nat := +Fixpoint max n m : nat := match n, m with | O, _ => m | S n', O => n |