diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 4046ef7aec..01e37c7c18 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,10 +195,9 @@ 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)) + let d' = List.map (fun name -> match pi2 d with + | None -> NamedDecl.LocalAssum (name, pi3 d) + | Some value -> NamedDecl.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 |