diff options
| author | Maxime Dénès | 2017-12-05 12:56:11 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-05 12:56:11 +0100 |
| commit | 2c5e81e3bc6ec17d253aeedd1b2bf4ccd3b81933 (patch) | |
| tree | 1e8d3db28d8d19b575e9e555f6ce379960c842c1 /vernac/command.mli | |
| parent | d403b2200ef32afd1eb1087a1f0ef2e6b8bb93f6 (diff) | |
| parent | 17b620f8bdf47a744d24513dcaef720d9160d443 (diff) | |
Merge PR #890: Global universe declarations
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 070f3e1120..a1f916c782 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -28,7 +28,7 @@ val do_constraint : polymorphic -> val interp_definition : Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * - Univdecls.universe_decl * Universes.universe_binders * Impargs.manual_implicits + Univdecls.universe_decl * Impargs.manual_implicits val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> local_binder_expr list -> red_expr option -> constr_expr -> |