aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith/Plus.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Arith/Plus.v')
-rw-r--r--theories/Arith/Plus.v2
1 files changed, 0 insertions, 2 deletions
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 9b7c62615..28613eecc 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
-
(** Properties of addition. [add] is defined in [Init/Peano.v] as:
<<
Fixpoint plus (n m:nat) : nat :=