diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 4046ef7aec..36d676f5d9 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -13,6 +13,9 @@ open Util open Pp open Printer +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (** Ide_slave : an implementation of [Interface], i.e. mainly an interp function and a rewind function. This specialized loop is triggered when the -ideslave option is passed to Coqtop. Currently CoqIDE is @@ -133,7 +136,8 @@ let annotate phrase = (** Goal display *) let hyp_next_tac sigma env decl = - let (id,_,ast) = Context.Named.Declaration.to_tuple decl in + let id = NamedDecl.get_id decl in + let ast = NamedDecl.get_type decl in let id_s = Names.Id.to_string id in let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in [ @@ -191,11 +195,7 @@ let process_goal sigma g = in let process_hyp d (env,l) = 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 + let d' = Context.NamedList.Declaration.to_named_context 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) = |