diff options
Diffstat (limited to 'theories/Arith/Div2.v')
-rw-r--r-- | theories/Arith/Div2.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 1f0c6c34b..42956c475 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -20,7 +20,7 @@ Implicit Type n : nat. (** Here we define [n/2] and prove some of its properties *) -Notation div2 := Nat.div2 (compat "8.4"). +Notation div2 := Nat.div2 (only parsing). (** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is useful to prove the corresponding induction principle *) @@ -86,7 +86,7 @@ Qed. (** Properties related to the double ([2n]) *) -Notation double := Nat.double (compat "8.4"). +Notation double := Nat.double (only parsing). Hint Unfold double Nat.double: arith. |