From d5d80dfc0f773fd6381ee4efefc74804d103fe4e Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 12 Aug 2016 17:46:18 +0200
Subject: CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple"
 function

---
 ide/ide_slave.ml | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

(limited to 'ide')

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
-- 
cgit v1.2.3