aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-07-01 21:59:00 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-07-01 21:59:00 +0000
commit7f110df7d7ff6a4d43f3c8d19305b20e24f4800e (patch)
tree506315cd644fe671eebea691941bdcb8baaa171b /library
parentf6007680bfa822ecc3d2f101fb6e21e2b1464b1b (diff)
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
Diffstat (limited to 'library')
-rw-r--r--library/lib.ml11
-rw-r--r--library/lib.mli1
2 files changed, 11 insertions, 1 deletions
diff --git a/library/lib.ml b/library/lib.ml
index bb0ad74ca..4743290ae 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
diff --git a/library/lib.mli b/library/lib.mli
index 80ce26fc6..c13f7f62d 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -173,6 +173,7 @@ val section_segment_of_constant : Names.constant -> Sign.named_context
val section_segment_of_mutual_inductive: Names.mutual_inductive -> Sign.named_context
val section_instance : Libnames.global_reference -> Names.identifier array
+val is_in_section : Libnames.global_reference -> bool
val add_section_variable : Names.identifier -> bool -> Term.types option -> unit
val add_section_constant : Names.constant -> Sign.named_context -> unit