diff options
| author | Maxime Dénès | 2017-06-19 17:43:19 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-19 17:43:19 +0200 |
| commit | 414890675cb72fd9286e19521a746677c06e784e (patch) | |
| tree | 14599a23215356ac472ac483ad564c11eb53c1fc /checker/declarations.ml | |
| parent | 396c77feb0cced3965f90f65c681e48c528636d5 (diff) | |
| parent | 15b1856edd593b39d63d23584a4f5acec0eeb592 (diff) | |
Merge PR#613: Cumulativity for inductive types
Diffstat (limited to 'checker/declarations.ml')
| -rw-r--r-- | checker/declarations.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index ad93146d55..2eefe47816 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -521,6 +521,11 @@ let subst_template_cst_arity sub (ctx,s as arity) = let subst_arity sub s = subst_decl_arity subst_mps subst_template_cst_arity sub s +let constant_is_polymorphic cb = + match cb.const_universes with + | Monomorphic_const _ -> false + | Polymorphic_const _ -> true + (* TODO: should be changed to non-coping after Term.subst_mps *) (* NB: we leave bytecode and native code fields untouched *) let subst_const_body sub cb = |