1 files changed, 12 insertions, 6 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index dc52ea9a..041f2f83 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -185,13 +185,15 @@ let process_goal sigma g =
   let ccl =
     let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
     string_of_ppcmds (pr_goal_concl_style_env env sigma norm_constr) in
-  let process_hyp d =
+  let process_hyp d (env,l) =
     let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in
-    (string_of_ppcmds (pr_var_list_decl min_env sigma d)) in
-  let hyps =
-    List.map process_hyp
-      (Termops.compact_named_context_reverse (Environ.named_context env)) in
-  { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
+    let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in
+      (List.fold_right Environ.push_named d' env,
+       (string_of_ppcmds (pr_var_list_decl env sigma d)) :: l) in
+  let (_env, hyps) =
+    Context.fold_named_list_context process_hyp
+      (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
+  { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
 
 let export_pre_goals pgs =
   {
@@ -289,11 +291,13 @@ let export_option_value = function
   | Goptions.BoolValue b   -> Interface.BoolValue b
   | Goptions.IntValue x    -> Interface.IntValue x
   | Goptions.StringValue s -> Interface.StringValue s
+  | Goptions.StringOptValue s -> Interface.StringOptValue s
 
 let import_option_value = function
   | Interface.BoolValue b   -> Goptions.BoolValue b
   | Interface.IntValue x    -> Goptions.IntValue x
   | Interface.StringValue s -> Goptions.StringValue s
+  | Interface.StringOptValue s -> Goptions.StringOptValue s
 
 let export_option_state s = {
   Interface.opt_sync  = s.Goptions.opt_sync;
@@ -312,6 +316,8 @@ let set_options options =
   | BoolValue b -> Goptions.set_bool_option_value name b
   | IntValue i -> Goptions.set_int_option_value name i
   | StringValue s -> Goptions.set_string_option_value name s
+  | StringOptValue (Some s) -> Goptions.set_string_option_value name s
+  | StringOptValue None -> Goptions.unset_option_value_gen None name
   in
   List.iter iter options