Various bug fix on recent features of the module system:

 - Include Self and equivalence of names
 - Include type in modules and nametab
 - Bang operator and composition of substitution



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

2 files changed, 66 insertions, 38 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 75a167f6c5..930d9aa7dd 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -140,12 +140,16 @@ let rec find_prefix resolve mp =
       sub_mp mp
     with
 	Not_found -> mp
-	  
+
+exception Change_equiv_to_inline of constr
+
 let solve_delta_kn resolve kn =
   try 
       match Deltamap.find (KN kn) resolve with
 	| Equiv kn1 -> kn1
-	| Inline _ -> raise Inline_kn
+	| Inline (Some c) -> 
+	    raise (Change_equiv_to_inline c)
+	| Inline None -> raise Inline_kn
 	| _ -> anomaly 
 	    "mod_subst: bad association in delta_resolver"
   with
@@ -160,39 +164,50 @@ let solve_delta_kn resolve kn =
 
 let constant_of_delta resolve con =
   let kn = user_con con in
-  let new_kn = solve_delta_kn resolve kn in
-    if kn == new_kn then
-      con
-    else
-      constant_of_kn_equiv kn new_kn
+    try 
+      let new_kn = solve_delta_kn resolve kn in
+	if kn == new_kn then
+	  con
+	else
+	  constant_of_kn_equiv kn new_kn
+    with 
+	_ -> con 
 	
 let constant_of_delta2 resolve con =
   let kn = canonical_con con in
   let kn1 = user_con con in
-  let new_kn = solve_delta_kn resolve kn in
-    if kn == new_kn then
-      con
-    else
-      constant_of_kn_equiv kn1 new_kn
+    try 
+      let new_kn = solve_delta_kn resolve kn in
+	if kn == new_kn then
+	  con
+	else
+	  constant_of_kn_equiv kn1 new_kn
+    with 
+	_ -> con
 
 let mind_of_delta resolve mind =
   let kn = user_mind mind in
-  let new_kn = solve_delta_kn resolve kn in
-    if kn == new_kn then
-      mind
-    else
-      mind_of_kn_equiv kn new_kn
-	
+    try
+      let new_kn = solve_delta_kn resolve kn in
+	if kn == new_kn then
+	  mind
+	else
+	  mind_of_kn_equiv kn new_kn
+    with 
+	_ -> mind 
+
 let mind_of_delta2 resolve mind =
   let kn = canonical_mind mind in
   let kn1 = user_mind mind in
-  let new_kn = solve_delta_kn resolve kn in
-    if kn == new_kn then
-      mind
-    else
-      mind_of_kn_equiv kn1 new_kn
-
-
+    try
+      let new_kn = solve_delta_kn resolve kn in
+	if kn == new_kn then
+	  mind
+	else
+	  mind_of_kn_equiv kn1 new_kn
+    with 
+	_ -> mind
+	  
 
 let inline_of_delta resolver = 
   let extract key hint l =
@@ -567,7 +582,11 @@ let subst_codom_delta_resolver subst resolver =
 	    Deltamap.fold Deltamap.add derived_resolve
 	      (Deltamap.add key (Prefix_equiv mpnew) resolver)
       | (Equiv kn) ->
-	  Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
+	  (try
+	     Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
+	   with
+	       Change_equiv_to_inline c ->
+		 Deltamap.add key (Inline (Some c)) resolver)
       | Inline None ->
 	  Deltamap.add key hint resolver
       | Inline (Some t) ->
@@ -585,10 +604,14 @@ let subst_dom_codom_delta_resolver subst resolver =
 	      (Deltamap.add key (Prefix_equiv mpnew) resolver)
       | (KN kn1),(Equiv kn) ->
 	  let key = KN (subst_kn subst kn1) in
-	  Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
+	    (try
+	       Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
+	     with
+		 Change_equiv_to_inline c ->
+		   Deltamap.add key (Inline (Some c)) resolver)
       | (KN kn),Inline None ->
 	  let key = KN (subst_kn subst kn) in
-	  Deltamap.add key hint resolver
+	    Deltamap.add key hint resolver
       | (KN kn),Inline (Some t) ->
 	  let key = KN (subst_kn subst kn) in
 	  Deltamap.add key (Inline (Some (subst_mps subst t))) resolver
@@ -607,9 +630,13 @@ let update_delta_resolver resolver1 resolver2 =
 		Prefix_equiv (find_prefix resolver2 mp)
 	      in Deltamap.add key new_hint res
 	  | Equiv kn ->
-	      let new_hint =
-		Equiv (solve_delta_kn resolver2 kn)
-	      in Deltamap.add key new_hint res
+	      (try 
+		 let new_hint =
+		   Equiv (solve_delta_kn resolver2 kn)
+		 in Deltamap.add key new_hint res
+	       with
+		   Change_equiv_to_inline c ->
+		     Deltamap.add key (Inline (Some c)) res)
 	  | _ -> Deltamap.add key hint res
       with not_found -> 
 	Deltamap.add key hint res
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e4c6ec35e1..d9c7c9de04 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -438,23 +438,24 @@ let end_module l restype senv =
    let senv = add_constraints cst senv in
    let mp_sup = senv.modinfo.modpath in
      (* Include Self support  *)
-   let rec compute_sign sign mb senv = 
+   let rec compute_sign sign mb resolver senv = 
      match sign with
      | SEBfunctor(mbid,mtb,str) ->
 	 let cst_sub = check_subtypes senv.env mb mtb in
 	 let senv = add_constraints cst_sub senv in
 	 let mpsup_delta = if not inl then mb.typ_delta else
-	   complete_inline_delta_resolver senv.env mp_sup mbid mtb mb.typ_delta
-	 in
+	   complete_inline_delta_resolver senv.env mp_sup mbid mtb mb.typ_delta in
+	 let subst = map_mbid mbid mp_sup mpsup_delta in
+	 let resolver = subst_codom_delta_resolver subst resolver in
 	   (compute_sign 
-	     (subst_struct_expr (map_mbid mbid mp_sup mpsup_delta) str) mb senv)
-     | str -> str,senv
+	     (subst_struct_expr subst str) mb resolver senv)
+     | str -> resolver,str,senv
    in
-   let sign,senv = compute_sign sign {typ_mp = mp_sup;
+   let resolver,sign,senv = compute_sign sign {typ_mp = mp_sup;
 				      typ_expr = SEBstruct (List.rev senv.revstruct);
 				      typ_expr_alg = None;
 				      typ_constraints = Constraint.empty;
-				      typ_delta = senv.modinfo.resolver} senv in
+				      typ_delta = senv.modinfo.resolver} resolver senv in
    let str = match sign with
      | SEBstruct(str_l) -> str_l
      | _ -> error ("You cannot Include a high-order structure.")