From e4282ea99c664d8d58067bee199cbbcf881b60d5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sat, 4 Jul 2009 13:28:35 +0200
Subject: Imported Upstream version 8.2.pl1+dfsg

---
 library/lib.ml | 22 ++++++++++++++--------
 1 file changed, 14 insertions(+), 8 deletions(-)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index 88bcd0b8..4a124cec 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: lib.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: lib.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
 
 open Pp
 open Util
@@ -452,7 +452,7 @@ type variable_context = variable_info list
 type abstr_list = variable_context Names.Cmap.t * variable_context Names.KNmap.t
 
 let sectab =
-  ref ([] : ((Names.identifier * binding_kind * Term.types option) list * Cooking.work_list * abstr_list) list)
+  ref ([] : ((Names.identifier * binding_kind * (Term.types * Names.identifier list) option) list * Cooking.work_list * abstr_list) list)
 
 let add_section () =
   sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab
@@ -460,13 +460,19 @@ let add_section () =
 let add_section_variable id impl keep =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
-    | (vars,repl,abs)::sl -> sectab := ((id,impl,keep)::vars,repl,abs)::sl
+    | (vars,repl,abs)::sl ->
+	sectab := ((id,impl,keep)::vars,repl,abs)::sl
 
-let rec extract_hyps = function
-  | ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: extract_hyps (idl,hyps)
-  | ((id,impl,Some ty)::idl,hyps) -> (id,impl,None,ty) :: extract_hyps (idl,hyps)
-  | (id::idl,hyps) -> extract_hyps (idl,hyps)
-  | [], _ -> []
+let extract_hyps (secs,ohyps) =
+  let rec aux = function
+    | ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: aux (idl,hyps)
+    | ((id,impl,Some (ty,keep))::idl,hyps) -> 
+	if List.exists (fun (id,_,_) -> List.mem id keep) ohyps then
+	  (id,impl,None,ty) :: aux (idl,hyps)
+	else aux (idl,hyps)
+    | (id::idl,hyps) -> aux (idl,hyps)
+    | [], _ -> []
+  in aux (secs,ohyps)
 
 let instance_from_variable_context sign =
   let rec inst_rec = function
-- 
cgit v1.2.3