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` --- checker/inductive.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'checker/inductive.mli') diff --git a/checker/inductive.mli b/checker/inductive.mli index 8f605935d..0170bbc94 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -31,7 +31,7 @@ val type_of_inductive : env -> mind_specif puniverses -> constr (* Return type as quoted by the user *) val type_of_constructor : pconstructor -> mind_specif -> constr -val arities_of_specif : mutual_inductive puniverses -> mind_specif -> constr array +val arities_of_specif : MutInd.t puniverses -> mind_specif -> constr array (* [type_case_branches env (I,args) (p:A) c] computes useful types about the following Cases expression: -- cgit v1.2.3