From 16ecabd99d66b3068e17fae486ba4ed77954e813 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Sun, 14 Aug 2016 13:26:55 +0200
Subject: CLEANUP: removing calls of the "Context.Named.Declaration.get_value"
 function

---
 tactics/equality.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index fcfd26185e..d078532b5d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1717,9 +1717,9 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
 let subst_one_var dep_proof_ok x =
   Proofview.Goal.enter { enter = begin fun gl ->
     let gl = Proofview.Goal.assume gl in
-    let xval = pf_get_hyp x gl |> NamedDecl.get_value in
+    let decl = pf_get_hyp x gl in
     (* If x has a body, simply replace x with body and clear x *)
-    if not (Option.is_empty xval) then tclTHEN (unfold_body x) (clear [x]) else
+    if is_local_def decl then tclTHEN (unfold_body x) (clear [x]) else
       (* Find a non-recursive definition for x *)
       let res =
         try
-- 
cgit v1.2.3