diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-12 22:31:42 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-12 22:31:42 +0000 |
commit | 5113afbb6e8c1f9122b37c37b0561c529c406256 (patch) | |
tree | 9087ea477f4de7f185d3468b0f13b1a23a3c39fc /checker/mod_checking.ml | |
parent | 62b92230d3ed0c01ce6cdb7bc59635ca7f659a9c (diff) |
Subtyping: align coqtop behavior concerning opaque csts on coqchk's one
After discussion with Bruno and Hugo, coqtop now accepts that an opaque
constant in a module type could be implemented by anything of
the right type, even if bodies differ. Said otherwise, with respect
to subtyping, an opaque constant behaves just as a parameter.
This was already the case in coqchk, and a footnote in documentation
is advertising for quite some time that:
"Opaque definitions are processed as assumptions."
Truly, it might seem awkward that "Definition x:=3" can implement
"Lemma x:nat. Proof 2. Qed." but the opacity ensures that nothing
can go wrong afterwards, since Coq is forced to ignore that the x
in signature has body "2".
Similarly, "T with Definition x := c" is now legal when T contains
an opaque x, even when this x isn't convertible with c.
By avoiding accesses to opaque bodies, we also achieve some speedup
(less delayed load of .vo final sections containing opaque terms).
Nota: the extraction will have to be adapted, since for the moment it
might access the body of opaque constants: the warning emitted when
doing that should become an error.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13987 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/mod_checking.ml')
-rw-r--r-- | checker/mod_checking.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index e6582e918..d35dfaff1 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -110,8 +110,11 @@ let check_definition_sub env cb1 cb2 = let typ1 = Typeops.type_of_constant_type env cb1.const_type in let typ2 = Typeops.type_of_constant_type env cb2.const_type in check_type env typ1 typ2; + (* In the spirit of subtyping.check_constant, we accept + any implementations of parameters and opaques terms, + as long as they have the right type *) (match cb2.const_body with - | Undef _ -> () + | Undef _ | OpaqueDef _ -> () | Def lc2 -> (match cb1.const_body with | Def lc1 -> @@ -119,8 +122,7 @@ let check_definition_sub env cb1 cb2 = let c2 = force_constr lc2 in Reduction.conv env c1 c2 (* Coq only places transparent cb in With_definition_body *) - | _ -> assert false) - | _ -> ()) (* Pierre L: shouldn't this case raise an error ? *) + | _ -> assert false)) let lookup_modtype mp env = try Environ.lookup_modtype mp env |