From f3abbc55ef160d1a65d4467bfe9b25b30b965a46 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 4 Nov 2017 18:58:27 +0100 Subject: [api] Deprecate all legacy uses of Names in core. This will allow to merge back `Names` with `API.Names` --- kernel/entries.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/entries.ml') diff --git a/kernel/entries.ml b/kernel/entries.ml index a1ccbdbc1..f294c4ce4 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -85,7 +85,7 @@ type parameter_entry = Context.Named.t option * bool * types Univ.in_universe_context * inline type projection_entry = { - proj_entry_ind : mutual_inductive; + proj_entry_ind : MutInd.t; proj_entry_arg : int } type 'a constant_entry = @@ -115,8 +115,8 @@ type seff_env = | `Opaque of Constr.t * Univ.universe_context_set ] type side_eff = - | SEsubproof of constant * Declarations.constant_body * seff_env - | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string + | SEsubproof of Constant.t * Declarations.constant_body * seff_env + | SEscheme of (inductive * Constant.t * Declarations.constant_body * seff_env) list * string type side_effect = { from_env : Declarations.structure_body CEphemeron.key; -- cgit v1.2.3