aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/mod_typing.ml8
-rw-r--r--kernel/subtyping.ml36
2 files changed, 14 insertions, 30 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index aad541d21..b8162340f 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -87,8 +87,11 @@ and check_with_aux_def env sign with_decl mp equiv =
| SFBconst cb -> cb
| _ -> error_not_a_constant l
in
+ (* 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 def,cst = match cb.const_body with
- | Undef _ ->
+ | Undef _ | OpaqueDef _ ->
let (j,cst1) = Typeops.infer env' c in
let typ = Typeops.type_of_constant_type env' cb.const_type in
let cst2 = Reduction.conv_leq env' j.uj_type typ in
@@ -104,9 +107,6 @@ and check_with_aux_def env sign with_decl mp equiv =
let cst = union_constraints cb.const_constraints cst1 in
let def = Def (Declarations.from_val c) in
def,cst
- | OpaqueDef _ ->
- (* We cannot make transparent an opaque field *)
- raise Reduction.NotConvertible
in
let cb' =
{ cb with
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index cac55f4be..2430dc6f0 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -260,39 +260,23 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
let typ1 = Typeops.type_of_constant_type env cb1.const_type in
let typ2 = Typeops.type_of_constant_type env cb2.const_type in
let cst = check_type cst env typ1 typ2 in
- (* Now we check the bodies *)
+ (* Now we check the bodies:
+ - A transparent constant can only be implemented by a compatible
+ transparent constant.
+ - In the signature, an opaque is handled just as a parameter:
+ anything of the right type can implement it, even if bodies differ.
+ *)
(match cb2.const_body with
- | Undef _ -> cst
+ | Undef _ | OpaqueDef _ -> cst
| Def lc2 ->
- (* Only a transparent cb1 can implement a transparent cb2.
- NB: cb1 might have been strengthened and appear as transparent.
- Anyway [check_conv] will handle that afterwards. *)
(match cb1.const_body with
| Undef _ | OpaqueDef _ -> error NotConvertibleBodyField
| Def lc1 ->
+ (* NB: cb1 might have been strengthened and appear as transparent.
+ Anyway [check_conv] will handle that afterwards. *)
let c1 = Declarations.force lc1 in
let c2 = Declarations.force lc2 in
- check_conv NotConvertibleBodyField cst conv env c1 c2)
- | OpaqueDef lc2 ->
- (* Here cb1 can be either opaque or transparent. We need to
- bypass the opacity and possibly do a delta step. *)
- (match body_of_constant cb1 with
- | None -> error NotConvertibleBodyField
- | Some lc1 ->
- let c1 = Declarations.force lc1 in
- let c2 = Declarations.force_opaque lc2 in
- let c1' = match (kind_of_term c1),(kind_of_term c2) with
- | Const n1,Const n2 when (eq_constant n1 n2) -> c1
- (* cb1 may have been strengthened, we need to unfold it: *)
- | Const n1,_ ->
- let cb1' = subst_const_body subst1 (lookup_constant n1 env)
- in
- (match cb1'.const_body with
- | OpaqueDef lc1' -> Declarations.force_opaque lc1'
- | _ -> c1)
- | _,_ -> c1
- in
- check_conv NotConvertibleBodyField cst conv env c1' c2))
+ check_conv NotConvertibleBodyField cst conv env c1 c2))
| IndType ((kn,i),mind1) ->
ignore (Util.error (
"The kernel does not recognize yet that a parameter can be " ^