merging conflicts with the original "trunk__CLEANUP__Context__2" branch

1 files changed, 8 insertions, 3 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 20cf48d7f8..12ef0e0751 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -130,7 +130,8 @@ let annotate phrase =
 
 (** Goal display *)
 
-let hyp_next_tac sigma env (id,_,ast) =
+let hyp_next_tac sigma env decl =
+  let (id,_,ast) = Context.Named.Declaration.to_tuple decl in
   let id_s = Names.Id.to_string id in
   let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in
   [
@@ -187,8 +188,12 @@ let process_goal sigma g =
     Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr)
   in
   let process_hyp d (env,l) =
-    let d = Context.NamedList.Declaration.map (Reductionops.nf_evar sigma) d in
-    let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in
+    let d = Context.NamedList.Declaration.map_constr (Reductionops.nf_evar sigma) d in
+    let d' = List.map (fun name -> let open Context.Named.Declaration in
+                                   match pi2 d with
+                                   | None -> LocalAssum (name, pi3 d)
+                                   | Some value -> LocalDef (name, value, pi3 d))
+                      (pi1 d) in
       (List.fold_right Environ.push_named d' env,
        (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in
   let (_env, hyps) =