diff options
| author | Emilio Jesus Gallego Arias | 2017-11-04 18:58:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-11-06 23:05:31 +0100 |
| commit | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (patch) | |
| tree | fceac407f6e4254e107817b6140257bcc8f9755a /vernac/command.mli | |
| parent | 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff) | |
[api] Deprecate all legacy uses of Names in core.
This will allow to merge back `Names` with `API.Names`
Diffstat (limited to 'vernac/command.mli')
| -rw-r--r-- | vernac/command.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/command.mli b/vernac/command.mli index afa97aa24f..26b1d1aaff 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -90,7 +90,7 @@ val interp_mutual_inductive : val declare_mutual_inductive_with_eliminations : mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list -> - mutual_inductive + MutInd.t (** Entry points for the vernacular commands Inductive and CoInductive *) |