aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--kernel/declareops.ml31
-rw-r--r--kernel/declareops.mli4
-rw-r--r--kernel/mod_typing.ml18
-rw-r--r--kernel/subtyping.ml31
-rw-r--r--library/global.ml4
-rw-r--r--library/global.mli4
-rw-r--r--printing/prettyp.ml20
7 files changed, 32 insertions, 80 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 9a75b1993..1337036b8 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -67,37 +67,6 @@ let type_of_constant cb =
if t' == t then x else RegularArity t'
| TemplateArity _ as x -> x
-let constraints_of_constant otab cb =
- match cb.const_universes with
- | Polymorphic_const ctx ->
- Univ.UContext.constraints (Univ.instantiate_univ_context ctx)
- | Monomorphic_const ctx ->
- Univ.Constraint.union
- (Univ.UContext.constraints ctx)
- (match cb.const_body with
- | Undef _ -> Univ.empty_constraint
- | Def c -> Univ.empty_constraint
- | OpaqueDef o ->
- Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o))
-
-let universes_of_constant otab cb =
- match cb.const_body with
- | Undef _ | Def _ ->
- begin
- match cb.const_universes with
- | Monomorphic_const ctx -> ctx
- | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
- end
- | OpaqueDef o ->
- let body_uctxs = Opaqueproof.force_constraints otab o in
- match cb.const_universes with
- | Monomorphic_const ctx ->
- let uctxs = Univ.ContextSet.of_context ctx in
- Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs)
- | Polymorphic_const ctx ->
- assert(Univ.ContextSet.is_empty body_uctxs);
- Univ.instantiate_univ_context ctx
-
let universes_of_polymorphic_constant otab cb =
match cb.const_universes with
| Monomorphic_const _ -> Univ.UContext.empty
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index d698d88b4..7350724b8 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -39,10 +39,6 @@ val constant_is_polymorphic : constant_body -> bool
val body_of_constant :
Opaqueproof.opaquetab -> constant_body -> Term.constr option
val type_of_constant : constant_body -> constant_type
-val constraints_of_constant :
- Opaqueproof.opaquetab -> constant_body -> Univ.constraints
-val universes_of_constant :
- Opaqueproof.opaquetab -> constant_body -> Univ.universe_context
(** Return the universe context, in case the definition is polymorphic, otherwise
the context is empty. *)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index f53ef6f56..71c037008 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -72,16 +72,13 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
(* In the spirit of subtyping.check_constant, we accept
any implementations of parameters and opaques terms,
as long as they have the right type *)
- let uctx = Declareops.universes_of_constant (opaque_tables env) cb in
- let uctx = (* Context of the spec *)
+ let c', univs, ctx' =
match cb.const_universes with
- | Monomorphic_const _ -> uctx
- | Polymorphic_const auctx ->
- Univ.instantiate_univ_context auctx
- in
- let c', univs, ctx' =
- if not (Declareops.constant_is_polymorphic cb) then
- let env' = Environ.push_context ~strict:true uctx env' in
+ | Monomorphic_const _ ->
+ (** We do not add the deferred constraints of the body in the
+ environment, because they do not appear in the type of the
+ definition. Any inconsistency will be raised at a later stage
+ when joining the environment. *)
let env' = Environ.push_context ~strict:true ctx env' in
let c',cst = match cb.const_body with
| Undef _ | OpaqueDef _ ->
@@ -94,7 +91,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
let c' = Mod_subst.force_constr cs in
c, Reduction.infer_conv env' (Environ.universes env') c c'
in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
- else
+ | Polymorphic_const uctx ->
+ let uctx = Univ.instantiate_univ_context uctx in
let cus, ccst = Univ.UContext.dest uctx in
let newus, cst = Univ.UContext.dest ctx in
let () =
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 44a1e6191..6f128d5d3 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -358,38 +358,17 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
let c2 = Mod_subst.force_constr lc2 in
check_conv NotConvertibleBodyField cst poly u infer_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."));
- let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in
- if Declareops.constant_has_body cb2 then error DefinitionFieldExpected;
- let u1 = inductive_polymorphic_instance mind1 in
- let arity1,cst1 = constrained_type_of_inductive env
- ((mind1,mind1.mind_packets.(i)),u1) in
- let cst2 =
- Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in
- let typ2 = Typeops.type_of_constant_type env cb2.const_type in
- let cst = Constraint.union cst (Constraint.union cst1 cst2) in
- let error = NotConvertibleTypeField (env, arity1, typ2) in
- check_conv error cst false Univ.Instance.empty infer_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."));
- let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in
- if Declareops.constant_has_body cb2 then error DefinitionFieldExpected;
- let u1 = inductive_polymorphic_instance mind1 in
- let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
- let cst2 =
- Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in
- let ty2 = Typeops.type_of_constant_type env cb2.const_type in
- let cst = Constraint.union cst (Constraint.union cst1 cst2) in
- let error = NotConvertibleTypeField (env, ty1, ty2) in
- check_conv error cst false Univ.Instance.empty infer_conv env ty1 ty2
+ "name.")
let rec check_modules cst env msb1 msb2 subst1 subst2 =
let mty1 = module_type_of_module msb1 in
diff --git a/library/global.ml b/library/global.ml
index dd7f23378..8b59c84dd 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -124,10 +124,6 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
let opaque_tables () = Environ.opaque_tables (env ())
let body_of_constant_body cb = Declareops.body_of_constant (opaque_tables ()) cb
let body_of_constant cst = body_of_constant_body (lookup_constant cst)
-let constraints_of_constant_body cb =
- Declareops.constraints_of_constant (opaque_tables ()) cb
-let universes_of_constant_body cb =
- Declareops.universes_of_constant (opaque_tables ()) cb
(** Operations on kernel names *)
diff --git a/library/global.mli b/library/global.mli
index c7ccabe1a..754fa1516 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -91,10 +91,6 @@ val mind_of_delta_kn : kernel_name -> mutual_inductive
val opaque_tables : unit -> Opaqueproof.opaquetab
val body_of_constant : constant -> Term.constr option
val body_of_constant_body : Declarations.constant_body -> Term.constr option
-val constraints_of_constant_body :
- Declarations.constant_body -> Univ.constraints
-val universes_of_constant_body :
- Declarations.constant_body -> Univ.universe_context
(** Global universe name <-> level mapping *)
type universe_names =
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index faa69f41e..15c0f80b9 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -511,7 +511,25 @@ let print_constant with_values sep sp =
let val_0 = Global.body_of_constant_body cb in
let typ = Declareops.type_of_constant cb in
let typ = ungeneralized_type_of_constant_type typ in
- let univs = Global.universes_of_constant_body cb in
+ let univs =
+ let otab = Global.opaque_tables () in
+ match cb.const_body with
+ | Undef _ | Def _ ->
+ begin
+ match cb.const_universes with
+ | Monomorphic_const ctx -> ctx
+ | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
+ end
+ | OpaqueDef o ->
+ let body_uctxs = Opaqueproof.force_constraints otab o in
+ match cb.const_universes with
+ | Monomorphic_const ctx ->
+ let uctxs = Univ.ContextSet.of_context ctx in
+ Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs)
+ | Polymorphic_const ctx ->
+ assert(Univ.ContextSet.is_empty body_uctxs);
+ Univ.instantiate_univ_context ctx
+ in
let ctx =
Evd.evar_universe_context_of_binders
(Universes.universe_binders_of_global (ConstRef sp))