From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 1 Feb 2009 00:54:40 +0100
Subject: Imported Upstream version 8.2~rc2+dfsg

---
 proofs/redexpr.ml | 21 ++++++++++++---------
 1 file changed, 12 insertions(+), 9 deletions(-)

(limited to 'proofs/redexpr.ml')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 072a38b6..ad8ee3a2 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: redexpr.ml 11094 2008-06-10 19:35:23Z herbelin $ *)
+(* $Id: redexpr.ml 11481 2008-10-20 19:23:51Z herbelin $ *)
 
 open Pp
 open Util
@@ -46,12 +46,13 @@ let set_strategy_one ref l  =
         Csymtable.set_transparent_const sp
     | _ -> ()
 
-let cache_strategy str =
+let cache_strategy (_,str) =
   List.iter 
     (fun (lev,ql) -> List.iter (fun q -> set_strategy_one q lev) ql)
     str
 
-let subst_strategy (_,subs,obj) =
+let subst_strategy (_,subs,(local,obj)) =
+  local,
   list_smartmap
     (fun (k,ql as entry) ->
       let ql' = list_smartmap (Mod_subst.subst_evaluable_reference subs) ql in
@@ -68,14 +69,16 @@ let map_strategy f l =
               Some q' -> q' :: ql
             | None -> ql) ql [] in
       if ql'=[] then str else (lev,ql')::str) l [] in
-  if l'=[] then None else Some l'
+  if l'=[] then None else Some (false,l')
 
-let export_strategy obj =
+let export_strategy (local,obj) =
+  if local then None else
   map_strategy (function
       EvalVarRef _ -> None
     | EvalConstRef _ as q -> Some q) obj
 
-let classify_strategy (_,obj) = Substitute obj
+let classify_strategy (_,(local,_ as obj)) = 
+  if local then Dispose else Substitute obj
 
 let disch_ref ref =
   match ref with
@@ -84,7 +87,8 @@ let disch_ref ref =
         if c==c' then Some ref else Some (EvalConstRef c')
     | _ -> Some ref
 
-let discharge_strategy (_,obj) =
+let discharge_strategy (_,(local,obj)) =
+  if local then None else
   map_strategy disch_ref obj
 
 let (inStrategy,outStrategy) =
@@ -98,8 +102,7 @@ let (inStrategy,outStrategy) =
 
 
 let set_strategy local str =
-  if local then cache_strategy str
-  else Lib.add_anonymous_leaf (inStrategy str)
+  Lib.add_anonymous_leaf (inStrategy (local,str))
 
 let _ = 
   Summary.declare_summary "Transparent constants and variables"
-- 
cgit v1.2.3