From 300293c119981054c95182a90c829058530a6b6f Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 25 Dec 2011 13:19:42 +0100
Subject: Imported Upstream version 8.3.pl3

---
 checker/modops.ml | 69 +++++++++++++++++++++++--------------------------------
 1 file changed, 29 insertions(+), 40 deletions(-)

(limited to 'checker/modops.ml')

diff --git a/checker/modops.ml b/checker/modops.ml
index 6d53803b..38aeaee2 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -111,7 +111,7 @@ and add_module mb env =
       | _ -> anomaly "Modops:the evaluation of the structure failed "
 
 
-let strengthen_const env mp_from l cb resolver = 
+let strengthen_const mp_from l cb resolver =
   match cb.const_opaque, cb.const_body with
   | false, Some _ -> cb
   | true, Some _ 
@@ -126,14 +126,14 @@ let strengthen_const env mp_from l cb resolver =
 	}
 	  
 
-let rec strengthen_mod env mp_from mp_to mb = 
+let rec strengthen_mod mp_from mp_to mb =
   if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then
     mb 
   else
     match mb.mod_type with
      | SEBstruct (sign) -> 
 	 let resolve_out,sign_out = 
-	   strengthen_sig env mp_from sign mp_to mb.mod_delta in
+	   strengthen_sig mp_from sign mp_to mb.mod_delta in
 	   { mb with
 	       mod_expr = Some (SEBident mp_to);
 	       mod_type = SEBstruct(sign_out);
@@ -145,60 +145,49 @@ let rec strengthen_mod env mp_from mp_to mb =
      | SEBfunctor _ -> mb
      | _ -> anomaly "Modops:the evaluation of the structure failed "
 	 
-and strengthen_sig env mp_from sign mp_to resolver =
+and strengthen_sig mp_from sign mp_to resolver =
   match sign with
     | [] -> empty_delta_resolver,[]
     | (l,SFBconst cb) :: rest ->
-	let item' = 
-	  l,SFBconst (strengthen_const env mp_from l cb resolver) in
-	let resolve_out,rest' =
-	  strengthen_sig env mp_from rest mp_to resolver in
-	  resolve_out,item'::rest'
+	let item' = l,SFBconst (strengthen_const mp_from l cb resolver) in
+	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+	resolve_out,item'::rest'
     | (_,SFBmind _ as item):: rest ->
-	let resolve_out,rest' = 
-	  strengthen_sig env mp_from rest mp_to resolver in
-	  resolve_out,item::rest'
+	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+	resolve_out,item::rest'
     | (l,SFBmodule mb) :: rest ->
 	let mp_from' = MPdot (mp_from,l) in
-	let mp_to' = MPdot(mp_to,l) in 
-	let mb_out = 
-	  strengthen_mod env mp_from' mp_to' mb in
+	let mp_to' = MPdot(mp_to,l) in
+	let mb_out = strengthen_mod mp_from' mp_to' mb in
 	let item' = l,SFBmodule (mb_out) in
-	let env' = add_module mb_out env in
-	let resolve_out,rest' = 
-	  strengthen_sig env' mp_from rest mp_to resolver in
-	  resolve_out
-	  (*add_delta_resolver resolve_out mb.mod_delta*),
-	item':: rest'
-    | (l,SFBmodtype mty as item) :: rest -> 
-	let env' = add_modtype 
-	  (MPdot(mp_from,l)) mty env
-	in
-	let resolve_out,rest' = 
-	  strengthen_sig env' mp_from rest mp_to resolver in
-	  resolve_out,item::rest'
-    
-let strengthen env mtb mp = 
+	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+	resolve_out, item'::rest'
+    | (l,SFBmodtype mty as item) :: rest ->
+	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+	resolve_out, item::rest'
+
+let strengthen mtb mp =
     match mtb.typ_expr with
-      | SEBstruct (sign) -> 
+      | SEBstruct (sign) ->
 	  let resolve_out,sign_out =
-	    strengthen_sig env mtb.typ_mp sign mp mtb.typ_delta in
-	    {mtb with
-	       typ_expr = SEBstruct(sign_out);
-	       typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
+	    strengthen_sig mtb.typ_mp sign mp mtb.typ_delta
+	  in
+	  {mtb with
+	    typ_expr = SEBstruct(sign_out);
+	    typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
 		(add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)}
       | SEBfunctor _ -> mtb
       | _ -> anomaly "Modops:the evaluation of the structure failed "
 
-let subst_and_strengthen mb mp env =
-  strengthen_mod env mb.mod_mp mp 
+let subst_and_strengthen mb mp =
+  strengthen_mod mb.mod_mp mp
     (subst_module (map_mp mb.mod_mp mp) mb)
 
 
-let module_type_of_module env mp mb =
+let module_type_of_module mp mb =
   match mp with
       Some mp ->
-	strengthen env {
+	strengthen {
 	  typ_mp = mp;
 	  typ_expr = mb.mod_type;
 	  typ_expr_alg = None;
-- 
cgit v1.2.3