From 7f110df7d7ff6a4d43f3c8d19305b20e24f4800e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 1 Jul 2008 21:59:00 +0000
Subject: Documentation Prop<=Set et Arguments Scope Global Correction au
 passage d'un bug de Arguments Scope Global

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

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index bb0ad74ca3..4743290ae9 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -484,13 +484,22 @@ let section_segment_of_constant con =
 let section_segment_of_mutual_inductive kn =
   Names.KNmap.find kn (snd (pi3 (List.hd !sectab)))
 
+let rec list_mem_assoc_in_triple x = function
+  | [] -> raise Not_found
+  | (a,_,_)::l -> compare a x = 0 or list_mem_assoc_in_triple x l
+
 let section_instance = function
-  | VarRef id -> [||]
+  | VarRef id ->
+      if list_mem_assoc_in_triple id (pi1 (List.hd !sectab)) then [||]
+      else raise Not_found
   | ConstRef con ->
       Names.Cmap.find con (fst (pi2 (List.hd !sectab)))
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
       Names.KNmap.find kn (snd (pi2 (List.hd !sectab)))
 
+let is_in_section ref =
+  try ignore (section_instance ref); true with Not_found -> false
+
 let init_sectab () = sectab := []
 let freeze_sectab () = !sectab
 let unfreeze_sectab s = sectab := s
-- 
cgit v1.2.3