From 17190de73ed6a91ae41fa98f8acd636514642857 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Mon, 6 Dec 2021 14:00:17 -0500
Subject: [PATCH] Use coqdoc syntax

---
 theories/numbers.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/numbers.v b/theories/numbers.v
index 8b282be1..4f723143 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -65,10 +65,10 @@ Proof. unfold lt. apply _. Qed.
 Lemma nat_le_sum (x y : nat) : x ≤ y ↔ ∃ z, y = x + z.
 Proof. split; [exists (y - x); lia | intros [z ->]; lia]. Qed.
 
-(* [Arith.Minus.minus_plus] is deprecated starting in 8.16 *)
+(** [Arith.Minus.minus_plus] is deprecated starting in 8.16 *)
 Lemma nat_minus_plus n m : n + m - n = m.
 Proof. lia. Qed.
-(* [Arith.Minus.le_plus_minus] is deprecated starting in 8.16 *)
+(** [Arith.Minus.le_plus_minus] is deprecated starting in 8.16 *)
 Lemma nat_le_plus_minus n m : n ≤ m → m = n + (m - n).
 Proof. lia. Qed.
 
-- 
GitLab