Ajout d'un comportement special du sous-typage pour les constantes opaques.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11082 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 37 insertions, 13 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a3df35ad5a..c39a42646f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -314,10 +314,11 @@ let add_module l me senv =
 let add_alias l mp senv =
   check_label l senv.labset; 
   let mp' = MPdot(senv.modinfo.modpath, l) in
-  (* we get all alias substitutions that comes from mp *)
-  let _,sub = translate_struct_entry senv.env (MSEident mp) in
+  (* we get all updated alias substitutions that comes from mp *)
+  let _,sub = Modops.update_subst senv.env (lookup_module mp senv.env) mp in
    (* we add the new one *)
   let mp1 = scrape_alias mp senv.env in
+  let sub = update_subst sub (map_mp mp' mp) in
   let sub = join (map_mp mp' mp1) sub in
   let env' = register_alias mp' mp senv.env in
     mp', { old = senv.old;
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index f5b3e87bdf..6354bb0fb6 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -254,19 +254,42 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
       let cst = check_type cst env typ1 typ2 in
       let con = make_con (MPself msid1) empty_dirpath l in
       let cst =
-       match cb2.const_body with
-         | None -> cst
-         | Some lc2 ->
-	     let c2 = Declarations.force lc2 in
-	     let c1 = match cb1.const_body with
-	       | Some lc1 -> Declarations.force lc1
-	       | None -> mkConst con
-	     in
-	       check_conv cst conv env c1 c2
+	if cb2.const_opaque then
+	  match cb2.const_body with
+            | None -> cst
+            | Some lc2 ->
+		let c2 = Declarations.force lc2 in
+		let c1 = match cb1.const_body with
+		  | Some lc1 -> 
+		      let c = Declarations.force lc1 in
+			begin
+			  match (kind_of_term c) with
+			      Const n -> 
+				let cb = lookup_constant n env in
+				  (match cb.const_opaque,
+				     cb.const_body with
+				       | true, Some lc1 -> 
+					   Declarations.force lc1
+				       | _,_ -> c)
+			    | _ -> c
+			end
+		  | None -> mkConst con
+		in
+		  check_conv cst conv env c1 c2
+	else
+	  match cb2.const_body with
+            | None -> cst
+            | Some lc2 ->
+		let c2 = Declarations.force lc2 in
+		let c1 = match cb1.const_body with
+		  | Some lc1 -> Declarations.force lc1
+		  | None -> mkConst con
+		in
+		  check_conv cst conv env c1 c2
       in
-       cst
+	cst
    | IndType ((kn,i),mind1) ->
-      ignore (Util.error (
+       ignore (Util.error (
        "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 " ^