diff options
Diffstat (limited to 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index be6c18810e..92a566b7c6 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -195,6 +195,7 @@ let subst_regular_ind_arity sub s = let subst_template_ind_arity sub s = s +(* FIXME records *) let subst_ind_arity = subst_decl_arity subst_regular_ind_arity subst_template_ind_arity |