diff options
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/global.mli b/library/global.mli index 4a993d1aa..16ed53785 100644 --- a/library/global.mli +++ b/library/global.mli @@ -56,6 +56,6 @@ val id_of_global : global_reference -> identifier val mind_is_recursive : inductive -> bool val mind_nconstr : inductive -> int val mind_nparams : inductive -> int -val mind_arity : inductive -> constr -val mind_lc : inductive -> constr array +val mind_nf_arity : inductive -> constr +val mind_nf_lc : inductive -> constr array |