diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-03 15:54:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-03 16:33:27 +0200 |
| commit | e123ec7621d06cde2b65755bab75b438b9f02664 (patch) | |
| tree | 1d114e7e03a8ff283fd7d4021cf0abfe36f22b25 /kernel/mod_typing.ml | |
| parent | 35e0f327405fb659c7ec5f9f7d26ea284aa45810 (diff) | |
Do not add original constraints to the environment in 'with Definition' check.
This was useless, because immediate constraints are assumed to already be in
the current environment, while deferred constraints are useless for the
conversion check of the definition types, as they only appear in the opaque
body.
This also clarifies a bit what is going on in the typing of module constraints
w.r.t. global universes.
Diffstat (limited to 'kernel/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 18 |
1 files changed, 8 insertions, 10 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 79016735b..20ca61530 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 () = |