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/indtypes.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/indtypes.mli')

diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index e4b7c086af..f5d0ed3f29 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -34,7 +34,7 @@ exception InductiveError of inductive_error
 
 (** The following function does checks on inductive declarations. *)
 
-val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
+val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
 
 (** The following enforces a system compatible with the univalent model *)
 
@@ -44,4 +44,4 @@ val is_indices_matter : unit -> bool
 val compute_projections : pinductive -> Id.t -> Id.t ->
   int -> Context.Rel.t -> int array -> int array -> 
   Context.Rel.t -> Context.Rel.t -> 
-  (constant array * projection_body array)
+  (Constant.t array * projection_body array)
-- 
cgit v1.2.3