From 91b86f564eecda6add2097305217ddd982968f8d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Feb 2018 16:25:59 +0100
Subject: [PATCH] Make `nat_cancel` comments Coqdoc.

---
 theories/nat_cancel.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/nat_cancel.v b/theories/nat_cancel.v
index 97f54376..6202dacc 100644
--- a/theories/nat_cancel.v
+++ b/theories/nat_cancel.v
@@ -1,6 +1,6 @@
 From stdpp Require Import numbers.
 
-(* The class [NatCancel m n m' n'] is a simple canceler for natural numbers
+(** The class [NatCancel m n m' n'] is a simple canceler for natural numbers
 implemented using type classes.
 
 Input: [m], [n]; output: [m'], [n'].
@@ -71,7 +71,7 @@ Global Instance nat_cancel_leaf_S_else m n m' n' :
   NatCancelLeaf m n m' n' → NatCancelLeaf m (S n) m' (S n') | 4.
 Proof. unfold NatCancelLeaf, NatCancel. omega. Qed.
 
-(* The instance [nat_cancel_S_both] is redundant, but may reduce proof search
+(** The instance [nat_cancel_S_both] is redundant, but may reduce proof search
 quite a bit, e.g. when canceling constants in constants. *)
 Global Instance nat_cancel_S_both m n m' n' :
   NatCancel m n m' n' → NatCancel (S m) (S n) m' n' | 1.
@@ -83,4 +83,4 @@ Proof. unfold NatCancel, MakeNatPlus. omega. Qed.
 Global Instance nat_cancel_S m m' m'' Sm' n n' n'' :
   NatCancel m n m' n' → NatCancelLeaf 1 n' m'' n'' →
   MakeNatS m'' m' Sm' → NatCancel (S m) n Sm' n'' | 3.
-Proof. unfold NatCancelLeaf, NatCancel, MakeNatS. omega. Qed.
\ No newline at end of file
+Proof. unfold NatCancelLeaf, NatCancel, MakeNatS. omega. Qed.
-- 
GitLab