From 6ab381a8b44923863f276608c623972331a0a82a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 29 May 2018 15:21:16 +0200
Subject: [PATCH] coqdoc

---
 theories/option.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/option.v b/theories/option.v
index 47357b29..d9a554d9 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -26,7 +26,7 @@ Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
 Instance: Params (@from_option) 3.
 Arguments from_option {_ _} _ _ !_ / : assert.
 
-(* The eliminator with the identity function. *)
+(** The eliminator with the identity function. *)
 Notation default := (from_option id).
 
 (** An alternative, but equivalent, definition of equality on the option
-- 
GitLab