aboutsummaryrefslogtreecommitdiff
path: root/vernac/comInductive.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/comInductive.mli')
-rw-r--r--vernac/comInductive.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index f23085a538..9df8f7c341 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -39,8 +39,8 @@ val do_mutual_inductive :
associated schemes *)
type one_inductive_impls =
- Impargs.manual_implicits (** for inds *)*
- Impargs.manual_implicits list (** for constrs *)
+ Impargs.manual_implicits (* for inds *) *
+ Impargs.manual_implicits list (* for constrs *)
val declare_mutual_inductive_with_eliminations :
mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->