diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-07 16:33:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 14:50:47 +0200 |
| commit | 0d9a91113c4112eece0680e433f435fdfb39ea4b (patch) | |
| tree | cf90d290a92c02a2297b3a13b77190db9aa4db70 /checker/subtyping.ml | |
| parent | b5ad6a80107f196fa8ffcc4f5dff58bea8c4f70e (diff) | |
Getting rid of simple calls to AUContext.instance.
This function breaks the abstraction barrier of abstract universe contexts,
as it provides a way to observe the bound names of such a context. We remove
all the uses that can be easily get rid of with the current API.
Diffstat (limited to 'checker/subtyping.ml')
| -rw-r--r-- | checker/subtyping.ml | 20 |
1 files changed, 5 insertions, 15 deletions
diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 5fd5510a7..303b18476 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -309,27 +309,17 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = force_constr lc2 in check_conv conv env c1 c2)) | IndType ((kn,i),mind1) -> - ignore (CErrors.user_err (Pp.str ( + CErrors.user_err (Pp.str ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ - "name."))); - if constant_has_body cb2 then error () ; - let u = inductive_polymorphic_instance mind1 in - let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in - let typ2 = Typeops.type_of_constant_type env cb2.const_type in - check_conv conv_leq env arity1 typ2 - | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (CErrors.user_err (Pp.str ( + "name.")) + | IndConstr (((kn,i),j),mind1) -> + CErrors.user_err (Pp.str ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ - "name."))); - if constant_has_body cb2 then error () ; - let u1 = inductive_polymorphic_instance mind1 in - let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in - let ty2 = Typeops.type_of_constant_type env cb2.const_type in - check_conv conv env ty1 ty2 + "name.")) let rec check_modules env msb1 msb2 subst1 subst2 = let mty1 = module_type_of_module None msb1 in |