From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 6 Nov 2017 23:27:09 +0100 Subject: [api] Move structures deprecated in the API to the core. We do up to `Term` which is the main bulk of the changes. --- vernac/declareDef.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/declareDef.mli') diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 5dea0ba27..01a87818a 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -15,5 +15,5 @@ val declare_definition : Id.t -> definition_kind -> Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits -> Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference -val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t -> +val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.UContext.t -> Id.t -> Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> Globnames.global_reference -- cgit v1.2.3