From 2089e310ab00d7cc662c1698a4c35f14e750e9fe Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 29 May 2009 16:31:29 +0000
Subject: Fix extract hyps to correctly discharge all hyps as described by keep
 lists.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12154 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/lib.ml | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/library/lib.ml b/library/lib.ml
index 356f90b227..9dbf7ddc01 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -463,14 +463,16 @@ let add_section_variable id impl keep =
     | (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,keep))::idl,hyps) -> 
-      if List.exists (fun (id,_,_) -> List.mem id keep) hyps then
-	(id,impl,None,ty) :: extract_hyps (idl,hyps)
-      else 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