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

---
 plugins/omega/coq_omega.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/omega')

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index d625e3076..c5c44ef20 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1697,8 +1697,8 @@ let destructure_hyps =
     let rec loop = function
       | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
       | decl::lit ->
-          let (i,_,t) = to_tuple decl in
-	  begin try match destructurate_prop t with
+          let i = get_id decl in
+	  begin try match destructurate_prop (get_type decl) with
 	  | Kapp(False,[]) -> elim_id i
           | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit
           | Kapp(Or,[t1;t2]) ->
-- 
cgit v1.2.3