diff options
Diffstat (limited to 'checker/inductive.ml')
| -rw-r--r-- | checker/inductive.ml | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index f890adba9a..1271a02b0e 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -54,10 +54,17 @@ let inductive_params (mib,_) = mib.mind_nparams (** Polymorphic inductives *) -let inductive_instance mib = - if mib.mind_polymorphic then - UContext.instance mib.mind_universes - else Instance.empty +let inductive_is_polymorphic mib = + match mib.mind_universes with + | Monomorphic_ind _ -> false + | Polymorphic_ind ctx -> true + | Cumulative_ind cumi -> true + +let inductive_is_cumulative mib = + match mib.mind_universes with + | Monomorphic_ind _ -> false + | Polymorphic_ind ctx -> false + | Cumulative_ind cumi -> true (************************************************************************) @@ -93,7 +100,7 @@ let instantiate_params full t u args sign = let full_inductive_instantiate mib u params sign = let dummy = Prop Null in - let t = mkArity (subst_instance_context u sign,dummy) in + let t = mkArity (Term.subst_instance_context u sign,dummy) in fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) let full_constructor_instantiate ((mind,_),u,(mib,_),params) t = @@ -199,7 +206,7 @@ let instantiate_universes env ctx ar argsorts = let type_of_inductive_gen env ((mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> - if not mib.mind_polymorphic then a.mind_user_arity + if not (inductive_is_polymorphic mib) then a.mind_user_arity else subst_instance_constr u a.mind_user_arity | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in |