diff options
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index cb6d7b1178..e42df6d9c5 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -41,7 +41,7 @@ val mis_ntypes : inductive_instance -> int val mis_nconstr : inductive_instance -> int val mis_nparams : inductive_instance -> int val mis_nrealargs : inductive_instance -> int -val mis_kelim : inductive_instance -> sorts list +val mis_kelim : inductive_instance -> elimination_sorts list val mis_recargs : inductive_instance -> (recarg list) array array val mis_recarg : inductive_instance -> (recarg list) array val mis_typename : inductive_instance -> identifier |