diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 19 | ||||
| -rw-r--r-- | ide/utils/config_file.ml | 3 |
2 files changed, 10 insertions, 12 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index bb8723dfe6..08f49ae5dd 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -13,6 +13,10 @@ open Util open Pp open Printer +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration +module CompactedDecl = Context.Compacted.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 +137,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 [ @@ -190,16 +195,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_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 = CompactedDecl.map_constr (Reductionops.nf_evar sigma) d in + let d' = CompactedDecl.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 + (Richpp.richpp_of_pp (pr_compacted_decl env sigma d)) :: l) in let (_env, hyps) = - Context.NamedList.fold process_hyp + Context.Compacted.fold 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; } diff --git a/ide/utils/config_file.ml b/ide/utils/config_file.ml index 4d0aabeb6a..e4c613913b 100644 --- a/ide/utils/config_file.ml +++ b/ide/utils/config_file.ml @@ -44,9 +44,6 @@ (* ******************************************************************************** *) (* This code is intended to be usable without any dependencies. *) -(* pipeline style, see for instance Raw.of_channel. *) -let (|>) x f = f x - (* as List.assoc, but applies f to the element matching [key] and returns the list where this element has been replaced by the result of f. *) let rec list_assoc_remove key f = function |