diff options
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/library/lib.ml b/library/lib.ml index f6b4a2458b..8880a8b154 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Libnames open Globnames @@ -428,8 +428,10 @@ let add_section_context ctx = sectab := (Context ctx :: vars,repl,abs)::sl let extract_hyps (secs,ohyps) = + let open Context.Named.Declaration in let rec aux = function - | (Variable (id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' -> + | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (get_id decl) -> + let (id',b,t) = to_tuple decl in let l, r = aux (idl,hyps) in (id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r | (Variable (_,_,poly,ctx)::idl,hyps) -> @@ -448,7 +450,10 @@ let instance_from_variable_context sign = | [] -> [] in Array.of_list (inst_rec sign) -let named_of_variable_context ctx = List.map (fun (id,_,b,t) -> (id,b,t)) ctx +let named_of_variable_context ctx = let open Context.Named.Declaration in + List.map (function id,_,None,t -> LocalAssum (id,t) + | id,_,Some b,t -> LocalDef (id,b,t)) + ctx let add_section_replacement f g poly hyps = match !sectab with @@ -478,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 |