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

---
 proofs/proof_using.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'proofs/proof_using.ml')

diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index caa9b328a0..5b24a1fb23 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -35,12 +35,14 @@ let in_nameset =
 let rec close_fwd e s =
   let s' =
     List.fold_left (fun s decl ->
-      let (id,b,ty) = Context.Named.Declaration.to_tuple decl in
-      let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in
-      let vty = global_vars_set e ty in
+      let vb = match decl with
+               | LocalAssum _ -> Id.Set.empty
+               | LocalDef (_,b,_) -> global_vars_set e b
+      in
+      let vty = global_vars_set e (get_type decl) in
       let vbty = Id.Set.union vb vty in
       if Id.Set.exists (fun v -> Id.Set.mem v s) vbty
-      then Id.Set.add id (Id.Set.union s vbty) else s)
+      then Id.Set.add (get_id decl) (Id.Set.union s vbty) else s)
     s (named_context e)
     in
   if Id.Set.equal s s' then s else close_fwd e s'
-- 
cgit v1.2.3