diff options
author | 2016-08-12 17:46:18 +0200 | |
---|---|---|
committer | 2016-08-24 17:35:20 +0200 | |
commit | d5d80dfc0f773fd6381ee4efefc74804d103fe4e (patch) | |
tree | 73be62f93b8716b5b69fadf705a91e106dadec17 /ide | |
parent | f5f4bb97634f4fac3dec766db27af994e745d749 (diff) |
CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function
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 4046ef7ae..01e37c7c1 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 |