From aa7a5ab6bdabd4205b64115fd2d803d2a06590a0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 2 Mar 2020 02:17:42 -0500
Subject: [lemmas] Fix comment on public API

After we moved `start_lemma_com` to `vernacentries` the comment on
`start_lemma_with_initialization` needs update.
---
 vernac/lemmas.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 79fdfe37de..67230e30f7 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -95,7 +95,7 @@ val start_dependent_lemma
 
 type lemma_possible_guards = int list list
 
-(** Pretty much internal, only used in ComFixpoint *)
+(** Pretty much internal, used by the Lemma / Fixpoint vernaculars *)
 val start_lemma_with_initialization
   :  ?hook:DeclareDef.Hook.t
   -> poly:bool
-- 
cgit v1.2.3