Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg

7 files changed, 268 insertions, 117 deletions

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 71a9aa0e..4e09a0ed 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -23,7 +23,7 @@ let patch_int buff pos n =
 
 let out_buffer = ref(String.create 1024)
 and out_position = ref 0
-
+(*
 let out_word b1 b2 b3 b4 =
   let p = !out_position in
   if p >= String.length !out_buffer then begin
@@ -37,6 +37,28 @@ let out_word b1 b2 b3 b4 =
   String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3);
   String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4);
   out_position := p + 4
+*)
+let out_word b1 b2 b3 b4 =
+  let p = !out_position in
+  if p >= String.length !out_buffer then begin
+    let len = String.length !out_buffer in
+    let new_len =
+      if len <= Sys.max_string_length / 2
+      then 2 * len
+      else
+	if len = Sys.max_string_length
+	then raise (Invalid_argument "String.create")  (* Pas la bonne execption
+.... *)
+	else Sys.max_string_length in
+    let new_buffer = String.create new_len in
+    String.blit !out_buffer 0 new_buffer 0 len;
+    out_buffer := new_buffer
+  end;
+  String.unsafe_set !out_buffer p (Char.unsafe_chr b1);
+  String.unsafe_set !out_buffer (p+1) (Char.unsafe_chr b2);
+  String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3);
+  String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4);
+  out_position := p + 4
 
 let out opcode =
   out_word opcode 0 0 0
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 6d2064bf..2942e101 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: mod_subst.ml 7538 2005-11-08 17:14:52Z herbelin $ *)
+(* $Id: mod_subst.ml 9874 2007-06-04 13:46:11Z soubiran $ *)
 
 open Pp
 open Util
@@ -25,7 +25,7 @@ let apply_opt_resolver resolve kn =
  match resolve with
     None -> None
   | Some resolve ->
-     try List.assoc kn resolve with Not_found -> assert false
+     try List.assoc kn resolve with Not_found -> None
 
 type substitution_domain = MSI of mod_self_id | MBI of mod_bound_id
 
@@ -110,6 +110,16 @@ let subst_con sub con =
           None -> con',mkConst con'
         | Some t -> con',t
 
+let subst_con0 sub con =
+ let mp,dir,l = repr_con con in
+  match subst_mp0 sub mp with
+      None -> None
+    | Some (mp',resolve) ->
+	let con' = make_con mp' dir l in
+       match apply_opt_resolver resolve con with
+           None -> Some (mkConst con')
+         | Some t -> Some t
+
 (* Here the semantics is completely unclear.
    What does "Hint Unfold t" means when "t" is a parameter?
    Does the user mean "Unfold X.t" or does she mean "Unfold y"
@@ -119,16 +129,14 @@ let subst_evaluable_reference subst = function
   | EvalVarRef id -> EvalVarRef id
   | EvalConstRef kn -> EvalConstRef (fst (subst_con subst kn))
 
-(* 
-This should be rewritten to prevent duplication of constr's when not
-necessary.
-For now, it uses map_constr and is rather ineffective
-*)
 
 let rec map_kn f f' c = 
   let func = map_kn f f' in
     match kind_of_term c with
-      | Const kn -> f' kn
+      | Const kn -> 
+	  (match f' kn with
+	       None -> c
+	     | Some const ->const)
       | Ind (kn,i) -> 
          (match f kn with
              None -> c
@@ -138,18 +146,64 @@ let rec map_kn f f' c =
          (match f kn with
              None -> c
            | Some kn' ->
-	      mkConstruct ((kn',i),j))
-      | Case (ci,p,c,l) ->
-	  let ci' =
-           { ci with
-              ci_ind =
-               let (kn,i) = ci.ci_ind in
-                match f kn with None -> ci.ci_ind | Some kn' -> kn',i } in
-	  mkCase (ci', func p, func c, array_smartmap func l) 
-      | _ -> map_constr func c
+	       mkConstruct ((kn',i),j))
+      | Case (ci,p,ct,l) -> 
+	  let ci_ind =
+            let (kn,i) = ci.ci_ind in
+              (match f kn with None -> ci.ci_ind | Some kn' -> kn',i ) in
+	  let p' = func p in
+	  let ct' = func ct in
+	  let l' = array_smartmap func l in
+	    if (ci.ci_ind==ci_ind && p'==p 
+		&& l'==l && ct'==ct)then c
+	    else 
+	      mkCase ({ci with ci_ind = ci_ind},
+		      p',ct', l')  
+      | Cast (ct,k,t) -> 
+	  let ct' = func ct in
+	  let t'= func t in
+	    if (t'==t && ct'==ct) then c 
+	    else mkCast (ct', k, t')
+      | Prod (na,t,ct) -> 
+	  let ct' = func ct in
+	  let t'= func t in
+	    if (t'==t && ct'==ct) then c 
+	    else mkProd (na, t', ct')
+      | Lambda (na,t,ct) -> 
+	  let ct' = func ct in
+	  let t'= func t in
+	    if (t'==t && ct'==ct) then c 
+	    else mkLambda (na, t', ct')
+      | LetIn (na,b,t,ct) -> 
+	  let ct' = func ct in
+	  let t'= func t in
+	  let b'= func b in
+	    if (t'==t && ct'==ct && b==b') then c 
+	    else mkLetIn (na, b', t', ct')
+      | App (ct,l) -> 
+	  let ct' = func ct in
+	  let l' = array_smartmap func l in
+	    if (ct'== ct && l'==l) then c
+	    else mkApp (ct',l')
+      | Evar (e,l) -> 
+	  let l' = array_smartmap func l in
+	    if (l'==l) then c
+	    else mkEvar (e,l')
+      | Fix (ln,(lna,tl,bl)) ->
+	  let tl' = array_smartmap func tl in
+	  let bl' = array_smartmap func bl in
+	    if (bl == bl'&& tl == tl') then c  
+	    else mkFix (ln,(lna,tl',bl'))
+      | CoFix(ln,(lna,tl,bl)) ->
+	  let tl' = array_smartmap func tl in
+	  let bl' = array_smartmap func bl in
+	    if (bl == bl'&& tl == tl') then c  
+	    else mkCoFix (ln,(lna,tl',bl'))
+      | _ -> c
+
 
 let subst_mps sub = 
-  map_kn (subst_kn0 sub) (fun con -> snd (subst_con sub con))
+  map_kn (subst_kn0 sub) (subst_con0 sub)
 
 let rec replace_mp_in_mp mpfrom mpto mp =
   match mp with
@@ -172,50 +226,57 @@ exception ChangeDomain of resolver
 let join (subst1 : substitution) (subst2 : substitution) = 
   let apply_subst (sub : substitution) key (mp,resolve) =
    let mp',resolve' =
-    match subst_mp0 sub mp with
-       None -> mp, None
-     | Some (mp',resolve') -> mp',resolve' in
+     match subst_mp0 sub mp with
+	 None -> mp, None
+       | Some (mp',resolve') -> mp',resolve' in
    let resolve'' : resolver option =
-    try
-     let res =
-      match resolve with
-         Some res -> res
-       | None ->
-          match resolve' with
-             None -> raise BothSubstitutionsAreIdentitySubstitutions
-           | Some res -> raise (ChangeDomain res)
-     in
-      Some
-       (List.map
-         (fun (kn,topt) ->
-           kn,
-           match topt with
-              None ->
-               (match key with
-                   MSI msid ->
-                    let kn' = replace_mp_in_con (MPself msid) mp kn in
-                     apply_opt_resolver resolve' kn'
-                 | MBI mbid ->
-                    let kn' = replace_mp_in_con (MPbound mbid) mp kn in
-                     apply_opt_resolver resolve' kn')
-            | Some t -> Some (subst_mps sub t)) res)
-    with
-       BothSubstitutionsAreIdentitySubstitutions -> None
-     | ChangeDomain res ->
-        Some
-         ((List.map
-            (fun (kn,topt) ->
-              let key' =
-               match key with
-                  MSI msid -> MPself msid
-                | MBI mbid -> MPbound mbid in
-              (* let's replace mp with key in kn *)
-              let kn' = replace_mp_in_con mp key' kn in
-               kn',topt)) res)
+     try
+       let res =
+	 match resolve with
+             Some res -> res
+	   | None ->
+               match resolve' with
+		   None -> raise BothSubstitutionsAreIdentitySubstitutions
+		 | Some res -> raise (ChangeDomain res)
+       in
+	 Some
+	   (List.map
+              (fun (kn,topt) ->
+		 kn,
+		 match topt with
+		     None ->
+		       (match key with
+			    MSI msid ->
+			      let kn' = replace_mp_in_con (MPself msid) mp kn in
+				apply_opt_resolver resolve' kn'
+			  | MBI mbid ->
+			      let kn' = replace_mp_in_con (MPbound mbid) mp kn in
+				apply_opt_resolver resolve' kn')
+		   | Some t -> Some (subst_mps sub t)) res)
+     with
+	 BothSubstitutionsAreIdentitySubstitutions -> None
+       | ChangeDomain res ->
+	   let rec changeDom = function
+	     | [] -> []
+	     | (kn,topt)::r ->
+		 let key' =
+		   match key with
+                       MSI msid -> MPself msid
+                     | MBI mbid -> MPbound mbid in
+		 let kn' = replace_mp_in_con mp key' kn in
+		   if kn==kn' then
+		     (*the key does not appear in mp, we remove it
+		       from the resolver that we are building*)
+		     changeDom r
+		   else
+		     (kn',topt)::(changeDom r)
+	   in
+	     Some (changeDom res)
    in
-    mp',resolve'' in
+     mp',resolve'' in
   let subst = Umap.mapi (apply_subst subst2) subst1 in
-  Umap.fold Umap.add subst2 subst
+    Umap.fold Umap.add subst2 subst
+ 
 
 let rec occur_in_path uid path =
  match uid,path with
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 352a1e46..70de3034 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mod_typing.ml 9558 2007-01-30 14:58:42Z soubiran $ i*)
+(*i $Id: mod_typing.ml 9980 2007-07-12 13:32:37Z soubiran $ i*)
 
 open Util
 open Names
@@ -131,8 +131,12 @@ and merge_with env mtb with_decl =
 	    let equiv = 
  	      match old.msb_equiv with
 		| None -> Some mp
-		| Some mp' -> 
-		    check_modpath_equiv env' mp mp';
+		| Some mp' ->
+		    begin
+		      try 
+			check_modpath_equiv env' mp mp'
+		      with Not_equiv_path -> error_not_equal mp mp
+		    end;
 		    Some mp
 	    in
 	    let msb =
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 8bab3c9d..fb00cfcd 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.ml 9558 2007-01-30 14:58:42Z soubiran $ i*)
+(*i $Id: modops.ml 9980 2007-07-12 13:32:37Z soubiran $ i*)
 
 (*i*)
 open Util
@@ -33,10 +33,11 @@ let error_not_a_functor _ = error "Application of not a functor"
 
 let error_incompatible_modtypes _ _ = error "Incompatible module types"
 
-let error_not_equal _ _ = error "Not equal modules"
-
-let error_not_match l _ = error ("Signature components for label "^string_of_label l^" do not match")
+let error_not_equal p1 p2 = error ((string_of_mp p1)^" and "^(string_of_mp p2)^" are not equal modules")
 
+let error_not_match l l1 l2 = error (l1^" is not a subtype of "^l2^": "^
+				       "Signature components for label "^(string_of_label l)^" do not match.")
+  
 let error_no_such_label l = error ("No such label "^string_of_label l)
 
 let error_incompatible_labels l l' = 
@@ -89,7 +90,7 @@ let error_circularity_in_subtyping l l1 l2 =
   error ("An occurrence of "^l^" creates a circularity\n during the subtyping verification between "^l1^" and "^l2^".")
 
 let error_no_such_label_sub l l1 l2 =
-  error (l1^" is not a subtype of "^l2^".\nThe field "^(string_of_label l)^" is missing (or invisible) in "^l1^".")
+  error (l1^" is not a subtype of "^l2^":"^"The field "^(string_of_label l)^" is missing in "^l1^".")
 
 
 let rec scrape_modtype env = function
@@ -124,6 +125,7 @@ let destr_functor = function
   | MTBfunsig (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t)
   | mtb -> error_not_a_functor mtb
  
+exception Not_equiv_path 
 
 let rec check_modpath_equiv env mp1 mp2 = 
   if mp1=mp2 then () else
@@ -132,7 +134,7 @@ let rec check_modpath_equiv env mp1 mp2 =
       | None ->
 	  let mb2 = lookup_module mp2 env in
 	    (match mb2.mod_equiv with
-	      | None -> error_not_equal mp1 mp2
+	      | None -> raise Not_equiv_path
 	      | Some mp2' -> check_modpath_equiv env mp2' mp1)
       | Some mp1' -> check_modpath_equiv env mp2 mp1'
 
@@ -244,16 +246,16 @@ and constants_of_modtype env mp modtype =
   | MTBfunsig _ -> []
 
 (* returns a resolver for kn that maps mbid to mp *)
-(* Nota: Some delta-expansions used to happen here. 
-    Browse SVN if you want to know more. *)
+(* Desactivated until v8.2, waiting for the integration
+of "Parameter Inline". *)
 let resolver_of_environment mbid modtype mp env =
  let constants = constants_of_modtype env (MPbound mbid) modtype in
- let resolve = List.map (fun (con,_) -> con,None) constants in 
- Mod_subst.make_resolver resolve
+ let _ = List.map (fun (con,_) -> con,None) constants in 
+ Mod_subst.make_resolver []
 
 
 let strengthen_const env mp l cb = 
-  match cb.const_opaque, cb.const_body with
+ match cb.const_opaque, cb.const_body with
   | false, Some _ -> cb
   | true, Some _ 
   | _, None -> 
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 55f81079..61761bb7 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.mli 9558 2007-01-30 14:58:42Z soubiran $ i*)
+(*i $Id: modops.mli 9980 2007-07-12 13:32:37Z soubiran $ i*)
 
 (*i*)
 open Util
@@ -21,6 +21,7 @@ open Mod_subst
 (* Various operations on modules and module types *)
 
 exception Circularity of string
+exception Not_equiv_path
 
 (* recursively unfold MTBdent module types *)
 val scrape_modtype : env -> module_type_body -> module_type_body
@@ -70,7 +71,7 @@ val error_incompatible_modtypes :
 
 val error_not_equal : module_path -> module_path -> 'a
 
-val error_not_match : label -> specification_body -> 'a
+val error_not_match : label -> string -> string -> 'a
   
 val error_incompatible_labels : label -> label -> 'a
 
diff --git a/kernel/names.ml b/kernel/names.ml
index 383d7879..4273fe14 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: names.ml 9558 2007-01-30 14:58:42Z soubiran $ *)
+(* $Id: names.ml 9980 2007-07-12 13:32:37Z soubiran $ *)
 
 open Pp
 open Util
@@ -65,7 +65,7 @@ let repr_dirpath x = x
 let empty_dirpath = []
 
 let string_of_dirpath = function
-  | [] -> "<empty>"
+  | [] -> ""
   | sl ->
       String.concat "." (List.map string_of_id (List.rev sl))
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index d1a10651..2e6e5a34 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtyping.ml 9558 2007-01-30 14:58:42Z soubiran $ i*)
+(*i $Id: subtyping.ml 10031 2007-07-19 18:05:46Z soubiran $ i*)
 
 (*i*)
 open Util
@@ -72,9 +72,11 @@ let check_conv_error error cst f env a1 a2 =
       NotConvertible -> error ()
 
 (* for now we do not allow reorderings *)
-let check_inductive cst env msid1 l info1 mib2 spec2 = 
+let check_inductive cst env msid1 l info1 mib2 spec2 path1 path2 = 
   let kn = make_kn (MPself msid1) empty_dirpath l in
-  let error () = error_not_match l spec2 in
+  let error () = error_not_match l
+    (String.concat "." (List.map string_of_id (List.rev path1)))
+    (String.concat "." (List.map string_of_id (List.rev path2))) in
   let check_conv cst f = check_conv_error error cst f in
   let mib1 = 
     match info1 with
@@ -192,8 +194,10 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
   in
     cst
     
-let check_constant cst env msid1 l info1 cb2 spec2 = 
-  let error () = error_not_match l spec2 in
+let check_constant cst env msid1 l info1 cb2 spec2 msid2 path1 path2 = 
+  let error () = error_not_match l
+    (String.concat "." (List.map string_of_id (List.rev path1)))
+    (String.concat "." (List.map string_of_id (List.rev path2))) in
   let check_conv cst f = check_conv_error error cst f in
   let check_type cst env t1 t2 = 
 
@@ -251,17 +255,53 @@ 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
+	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
+		begin
+		  match cb1.const_opaque,cb2.const_opaque with
+		      false,false |true,true ->
+			check_conv cst conv env c1 c2
+		    | false,true -> 
+			begin
+			  match kind_of_term c1 with
+			    | Const con' ->
+				let c1 = 
+				  match (Pre_env.lookup_constant con' 
+					   (pre_env env)).const_body with
+				      Some c -> Declarations.force c
+				    | None -> mkConst con'
+				in
+				  check_conv cst conv env c1 c2
+			    | _ ->
+				check_conv cst conv env c1 c2
+			end
+		    | true,false->
+			begin
+			  match (kind_of_term c2) with
+			    | Const con'-> 
+				if con' = con 
+				then cst
+				else
+				let c2 = 
+				  match (Pre_env.lookup_constant con' 
+					   (pre_env env)).const_body with
+				      Some c -> Declarations.force c
+				    | None -> mkConst con'
+				in
+				  check_conv cst conv env c1 c2
+			    | _ ->
+				check_conv cst conv env c1 c2
+			end
+		end
+		  
       in
-       cst
+	cst
    | IndType ((kn,i),mind1) ->
       ignore (Util.error (
        "The kernel does not recognize yet that a parameter can be " ^
@@ -286,60 +326,77 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
        check_conv cst conv env ty1 ty2
    | _ -> error ()
 	      
-let rec check_modules cst env msid1 l msb1 msb2 =
+let rec check_modules cst env msid1 l msb1 msb2 path1 path2 =
   let mp = (MPdot(MPself msid1,l)) in
   let mty1 = strengthen env msb1.msb_modtype mp in
-  let cst = check_modtypes cst env mty1 msb2.msb_modtype false in
-  begin
-    match msb1.msb_equiv, msb2.msb_equiv with
-      | _, None -> ()
-      | None, Some mp2 -> 
-	  check_modpath_equiv env mp mp2
-      | Some mp1, Some mp2 ->
-	  check_modpath_equiv env mp1 mp2
-  end;
-  cst
+  let cst = check_modtypes cst env mty1 msb2.msb_modtype false 
+    path1 path2 in
+    begin
+      match msb1.msb_equiv, msb2.msb_equiv with
+	| _, None -> ()
+	| None, Some mp2 -> 
+	    begin  
+	      try
+		check_modpath_equiv env mp mp2
+	      with Not_equiv_path -> error_not_equal mp mp2
+	    end
+	| Some mp1, Some mp2 -> try
+	    check_modpath_equiv env mp1 mp2
+	  with Not_equiv_path -> error_not_equal mp1 mp2
+    end;
+    cst
 	
 
-and check_signatures cst env (msid1,sig1) (msid2,sig2') = 
+and check_signatures cst env (msid1,sig1) (msid2,sig2') path1 path2= 
   let mp1 = MPself msid1 in
   let env = add_signature mp1 sig1 env in 
   let sig2 = try
     subst_signature_msid msid2 mp1 sig2' 
     with
     | Circularity l -> 
-	error_circularity_in_subtyping l (string_of_msid msid1) (string_of_msid msid2) in
+	error_circularity_in_subtyping l
+	  (String.concat "." (List.map string_of_id (List.rev path1)))
+	  (String.concat "." (List.map string_of_id (List.rev path2)))
+  in
   let map1 = make_label_map mp1 sig1 in
   let check_one_body cst (l,spec2) = 
     let info1 = 
       try 
 	Labmap.find l map1 
       with 
-	  Not_found -> error_no_such_label_sub l (string_of_msid msid1) (string_of_msid msid2)
+	  Not_found -> error_no_such_label_sub l 
+	    (String.concat "." (List.map string_of_id (List.rev path1)))
+	    (String.concat "." (List.map string_of_id (List.rev path2)))
     in
       match spec2 with
 	| SPBconst cb2 ->
-	    check_constant cst env msid1 l info1 cb2 spec2
+	    check_constant cst env msid1 l info1 cb2 spec2 msid2 path1 path2
 	| SPBmind mib2 -> 
-	    check_inductive cst env msid1 l info1 mib2 spec2
+	    check_inductive cst env msid1 l info1 mib2 spec2 path1 path2
 	| SPBmodule msb2 -> 
 	    let msb1 = 
 	      match info1 with
 		| Module msb -> msb
-		| _ -> error_not_match l spec2
+		| _ -> error_not_match l 
+		    (String.concat "." (List.map string_of_id (List.rev path1)))
+		      (String.concat "." (List.map string_of_id (List.rev path2)))
+
 	    in
-	      check_modules cst env msid1 l msb1 msb2
+	      check_modules cst env msid1 l msb1 msb2 path1 path2
 	| SPBmodtype mtb2 ->
 	    let mtb1 = 
 	      match info1 with
 		| Modtype mtb -> mtb
-		| _ -> error_not_match l spec2
+		| _ -> error_not_match l 
+		    (String.concat "." (List.map string_of_id (List.rev path1)))
+		      (String.concat "." (List.map string_of_id (List.rev path2)))
+
 	    in
-	      check_modtypes cst env mtb1 mtb2 true
+	      check_modtypes cst env mtb1 mtb2 true path1 path2
   in
     List.fold_left check_one_body cst sig2
     
-and check_modtypes cst env mtb1 mtb2 equiv = 
+and check_modtypes cst env mtb1 mtb2 equiv path1 path2 = 
   if mtb1==mtb2 then cst else (* just in case  :) *)
   let mtb1' = scrape_modtype env mtb1 in
   let mtb2' = scrape_modtype env mtb2 in
@@ -347,14 +404,17 @@ and check_modtypes cst env mtb1 mtb2 equiv =
     match mtb1', mtb2' with
       | MTBsig (msid1,list1), 
 	MTBsig (msid2,list2) -> 
-	  let cst = check_signatures cst env (msid1,list1) (msid2,list2) in
+	  let cst = check_signatures cst env (msid1,list1) (msid2,list2)
+	    ((id_of_msid msid1)::path1) ((id_of_msid msid2)::path2) in
 	  if equiv then
 	    check_signatures cst env (msid2,list2) (msid1,list1) 
+	      ((id_of_msid msid2)::path2) ((id_of_msid msid1)::path1)
 	  else
 	    cst
       | MTBfunsig (arg_id1,arg_t1,body_t1), 
 	MTBfunsig (arg_id2,arg_t2,body_t2) ->
-	  let cst = check_modtypes cst env arg_t2 arg_t1 equiv in 
+	  let cst = check_modtypes cst env arg_t2 arg_t1 equiv 
+	  [] [] in 
 	    (* contravariant *)
 	  let env = 
 	    add_module (MPbound arg_id2) (module_body_of_type arg_t2) env 
@@ -367,9 +427,10 @@ and check_modtypes cst env mtb1 mtb2 equiv =
 	      body_t1
 	  in
 	  check_modtypes cst env body_t1' body_t2 equiv
+	    path1 path2
       | MTBident _ , _ -> anomaly "Subtyping: scrape failed"
       | _ , MTBident _ -> anomaly "Subtyping: scrape failed"
       | _ , _ -> error_incompatible_modtypes mtb1 mtb2
 	  
 let check_subtypes env sup super = 
-  check_modtypes Constraint.empty env sup super false
+  check_modtypes Constraint.empty env sup super false [] []