From 2cb1fa87579542ff5dfbd8455c33ed65de9e1144 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 27 Nov 2000 11:32:31 +0000
Subject: Bug extract_instance en présence de défs locales

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@985 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declare.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/library/declare.ml b/library/declare.ml
index b3027a3a11..b6da493208 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -334,9 +334,10 @@ let extract_instance ref args =
   let hyps0 = current_section_context () in
   let na = Array.length args in
   let rec peel n acc = function
-    | d::hyps ->
+    | (_,None,_ as d)::hyps ->
 	if List.mem d hyps0 then peel (n-1) acc hyps
 	else peel (n-1) (args.(n)::acc) hyps
+    | (_,Some _,_)::hyps -> peel n acc hyps
     | [] -> Array.of_list acc
   in peel (na-1) [] hyps
 
-- 
cgit v1.2.3