diff options
| author | Maxime Dénès | 2017-07-28 18:23:46 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-28 18:23:46 +0200 |
| commit | e8bb8ea0da02b926e076cf04ea1c82c547a30ea2 (patch) | |
| tree | 1eadb6305528d826955cecc9b4dd6bcaccc0be86 /kernel/environ.ml | |
| parent | 3828267b6dcd60088a11fe0b9613871e4fc7c54f (diff) | |
| parent | d9530632321c0b470ece6337cda2cf54d02d61eb (diff) | |
Merge PR #889: Removing template polymorphism for definitions.
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 21 |
1 files changed, 3 insertions, 18 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index b01b652001..d2c737ab0c 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -232,12 +232,6 @@ let constraints_of cb u = | Monomorphic_const _ -> Univ.Constraint.empty | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx -let map_regular_arity f = function - | RegularArity a as ar -> - let a' = f a in - if a' == a then ar else RegularArity a' - | TemplateArity _ -> assert false - (* constant_type gives the type of a constant *) let constant_type env (kn,u) = let cb = lookup_constant kn env in @@ -245,7 +239,7 @@ let constant_type env (kn,u) = | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty | Polymorphic_const ctx -> let csts = constraints_of cb u in - (map_regular_arity (subst_instance_constr u) cb.const_type, csts) + (subst_instance_constr u cb.const_type, csts) let constant_context env kn = let cb = lookup_constant kn env in @@ -287,7 +281,7 @@ let constant_value_and_type env (kn, u) = | OpaqueDef _ -> None | Undef _ -> None in - b', map_regular_arity (subst_instance_constr u) cb.const_type, cst + b', subst_instance_constr u cb.const_type, cst else let b' = match cb.const_body with | Def l_body -> Some (Mod_subst.force_constr l_body) @@ -303,7 +297,7 @@ let constant_value_and_type env (kn, u) = let constant_type_in env (kn,u) = let cb = lookup_constant kn env in if Declareops.constant_is_polymorphic cb then - map_regular_arity (subst_instance_constr u) cb.const_type + subst_instance_constr u cb.const_type else cb.const_type let constant_value_in env (kn,u) = @@ -337,15 +331,6 @@ let polymorphic_pconstant (cst,u) env = let type_in_type_constant cst env = not (lookup_constant cst env).const_typing_flags.check_universes -let template_polymorphic_constant cst env = - match (lookup_constant cst env).const_type with - | TemplateArity _ -> true - | RegularArity _ -> false - -let template_polymorphic_pconstant (cst,u) env = - if not (Univ.Instance.is_empty u) then false - else template_polymorphic_constant cst env - let lookup_projection cst env = match (lookup_constant (Projection.constant cst) env).const_proj with | Some pb -> pb |