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

1 files changed, 10 insertions, 7 deletions

diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index e00671b03..50d27ce2c 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -243,20 +243,23 @@ let check_constant 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
 	check_type env typ1 typ2;
-	(* 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 _ -> ()
+	  | Undef _ | OpaqueDef _ -> ()
 	  | 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 ()
 	      | Def lc1 ->
+	        (* NB: cb1 might have been strengthened and appear as transparent.
+	           Anyway [check_conv] will handle that afterwards. *)
 		let c1 = force_constr lc1 in
 		let c2 = force_constr lc2 in
-		check_conv conv env c1 c2)
-	  | OpaqueDef lc2 -> ()) (* Pierre L. : this looks really strange ?! *)
+		check_conv conv env c1 c2))
       | IndType ((kn,i),mind1) ->
 	  ignore (Util.error (
 		    "The kernel does not recognize yet that a parameter can be " ^