diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-05-09 14:37:42 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-05-09 14:37:42 +0000 |
| commit | 8b0bab9313d9b26e6c9f132e82473b4db9a4832d (patch) | |
| tree | dc352810c9df3c47aa0ccb9198e3e8dfd0fd3a10 /kernel/inductive.mli | |
| parent | 0f23050eaf1271fc143c8698e830d83c2240926c (diff) | |
nettoyage extraction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1737 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 00c0dfbdb..cb6d7b117 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -52,6 +52,7 @@ val mis_consnames : inductive_instance -> identifier array val mis_conspaths : inductive_instance -> section_path array val mis_inductive : inductive_instance -> inductive val mis_arity : inductive_instance -> types +val mis_nf_arity : inductive_instance -> types val mis_params_ctxt : inductive_instance -> rel_context val mis_sort : inductive_instance -> sorts val mis_constructor_type : int -> inductive_instance -> types |