From d93becea84ab011fe9f7346c110b31e21eb823ee Mon Sep 17 00:00:00 2001
From: regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 27 Aug 2010 12:43:48 +0000
Subject: * (checker|kernel)/Safe_typing:   Rename "lighten_*" into
 "traverse_*" inside the [traverse_library]   function.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13385 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/safe_typing.ml | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 43090c8e1..51850eaab 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -864,39 +864,39 @@ end = struct
   (* Map a [compiled_library] to another one by just updating 
      the opaque term [t] to [on_opaque_const_body t]. *)
   let traverse_library on_opaque_const_body =
-    let rec lighten_module mb =
+    let rec traverse_module mb =
       { mb with
-	mod_expr = Option.map lighten_modexpr mb.mod_expr;
-	mod_type = lighten_modexpr mb.mod_type;
+	mod_expr = Option.map traverse_modexpr mb.mod_expr;
+	mod_type = traverse_modexpr mb.mod_type;
       }
-    and lighten_struct struc =
-      let lighten_body (l,body) = (l,match body with
+    and traverse_struct struc =
+      let traverse_body (l,body) = (l,match body with
 	| SFBconst ({const_opaque=true} as x) -> 
 	  SFBconst {x with const_body = on_opaque_const_body x.const_body }
 	| (SFBconst _ | SFBmind _ ) as x -> 
 	  x
 	| SFBmodule m -> 
-	  SFBmodule (lighten_module m)
+	  SFBmodule (traverse_module m)
 	| SFBmodtype m -> 
-	  SFBmodtype ({m with typ_expr = lighten_modexpr m.typ_expr}))
+	  SFBmodtype ({m with typ_expr = traverse_modexpr m.typ_expr}))
       in
-      List.map lighten_body struc
+      List.map traverse_body struc
 	
-    and lighten_modexpr = function
+    and traverse_modexpr = function
       | SEBfunctor (mbid,mty,mexpr) ->
 	SEBfunctor (mbid,
 		    ({mty with
-		      typ_expr = lighten_modexpr mty.typ_expr}),
-		    lighten_modexpr mexpr)
+		      typ_expr = traverse_modexpr mty.typ_expr}),
+		    traverse_modexpr mexpr)
       | SEBident mp as x -> x
       | SEBstruct (struc) ->
-	SEBstruct  (lighten_struct struc)
+	SEBstruct  (traverse_struct struc)
       | SEBapply (mexpr,marg,u) ->
-	SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u)
+	SEBapply (traverse_modexpr mexpr,traverse_modexpr marg,u)
       | SEBwith (seb,wdcl) ->
-	SEBwith (lighten_modexpr seb,wdcl)
+	SEBwith (traverse_modexpr seb,wdcl)
     in
-    fun (dp,mb,depends,s) -> (dp,lighten_module mb,depends,s) 
+    fun (dp,mb,depends,s) -> (dp,traverse_module mb,depends,s) 
 
   (* To disburden a library from opaque definitions, we simply 
      traverse it and add an indirection between the module body 
-- 
cgit v1.2.3