diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index db2f57d67c..ec88720fc1 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -447,9 +447,9 @@ let add_mind sp mie env = let (ind',cst') = type_one_inductive i env_arities env_params nparams ninds ind in - (succ i,ind'::inds, Constraint.union cst cst')) + (i-1,ind'::inds, Constraint.union cst cst')) mie.mind_entry_inds - (1,[],Constraint.empty) + (ninds,[],Constraint.empty) in let kind = kind_of_path sp in let mib = |