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

---
 plugins/decl_mode/decl_proof_instr.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 97c9d5f4a2..6a28723b89 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -821,9 +821,8 @@ let define_tac id args body gls =
 
 let cast_tac id_or_thesis typ gls =
   match id_or_thesis with
-      This id ->
-	let body = pf_get_hyp gls id |> get_value in
-	  Proofview.V82.of_tactic (convert_hyp (of_tuple (id,body,typ))) gls
+    | This id ->
+        Proofview.V82.of_tactic  (pf_get_hyp gls id |> set_id id |> set_type typ |> convert_hyp) gls
     | Thesis (For _ ) ->
 	error "\"thesis for ...\" is not applicable here."
     | Thesis Plain ->
-- 
cgit v1.2.3