merging conflicts with the original "trunk__CLEANUP__Context__2" branch

1 files changed, 7 insertions, 2 deletions

diff --git a/library/lib.ml b/library/lib.ml
index e4617cafb6..f8bb6bac59 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -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