From 1297523bffdc3a9fe3e447acc6837be835e86d06 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 15 Aug 2016 14:14:14 +0200
Subject: CLEANUP: changing the definition of the
 "Context.NamedList.Declaration" type

---
 ide/ide_slave.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'ide')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 01e37c7c18..36d676f5d9 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -195,10 +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 -> match pi2 d with
-                                   | None -> NamedDecl.LocalAssum (name, pi3 d)
-                                   | Some value -> NamedDecl.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) =
-- 
cgit v1.2.3