From 4965fa03bd9cbc37dd6888c7d13c3fba83b2652c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 29 Jun 2016 11:28:55 +0200
Subject: Exporting section_segment_of_reference.

---
 library/impargs.ml | 10 ++--------
 library/lib.ml     |  6 ++++++
 library/lib.mli    |  3 ++-
 3 files changed, 10 insertions(+), 9 deletions(-)

(limited to 'library')

diff --git a/library/impargs.ml b/library/impargs.ml
index 4e344a954..feb3bf018 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -526,12 +526,6 @@ let impls_of_context ctx =
   in
   List.rev_map map (List.filter is_set ctx)
 
-let section_segment_of_reference = function
-  | ConstRef con -> pi1 (section_segment_of_constant con)
-  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-    pi1 (section_segment_of_mutual_inductive kn)
-  | _ -> []
-
 let adjust_side_condition p = function
   | LessArgsThan n -> LessArgsThan (n+p)
   | DefaultImpArgs -> DefaultImpArgs
@@ -545,7 +539,7 @@ let discharge_implicits (_,(req,l)) =
   | ImplLocal -> None
   | ImplInteractive (ref,flags,exp) ->
     (try
-      let vars = section_segment_of_reference ref in
+      let vars = variable_section_segment_of_reference ref in
       let ref' = if isVarRef ref then ref else pop_global_reference ref in
       let extra_impls = impls_of_context vars in
       let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
@@ -563,7 +557,7 @@ let discharge_implicits (_,(req,l)) =
   | ImplMutualInductive (kn,flags) ->
     (try
       let l' = List.map (fun (gr, l) ->
-	let vars = section_segment_of_reference gr in
+	let vars = variable_section_segment_of_reference gr in
 	let extra_impls = impls_of_context vars in
 	((if isVarRef gr then gr else pop_global_reference gr),
 	 List.map (add_section_impls vars extra_impls) l)) l
diff --git a/library/lib.ml b/library/lib.ml
index f580050db..23a2d4846 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -483,6 +483,12 @@ let section_segment_of_constant con =
 let section_segment_of_mutual_inductive kn =
   Names.Mindmap.find kn (snd (pi3 (List.hd !sectab)))
 
+let variable_section_segment_of_reference = function
+  | ConstRef con -> pi1 (section_segment_of_constant con)
+  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+      pi1 (section_segment_of_mutual_inductive kn)
+  | _ -> []
+                     
 let section_instance = function
   | VarRef id ->
      let eq = function
diff --git a/library/lib.mli b/library/lib.mli
index e2e71ac90..7080b5dba 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -172,7 +172,8 @@ val named_of_variable_context : variable_context -> Context.Named.t
 
 val section_segment_of_constant : Names.constant -> abstr_info
 val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info
-
+val variable_section_segment_of_reference : Globnames.global_reference -> variable_context
+                                                                                                     
 val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array
 val is_in_section : Globnames.global_reference -> bool
 
-- 
cgit v1.2.3