diff options
| author | Matej Kosik | 2016-08-14 13:26:55 +0200 |
|---|---|---|
| committer | Matej Kosik | 2016-08-25 00:09:17 +0200 |
| commit | 16ecabd99d66b3068e17fae486ba4ed77954e813 (patch) | |
| tree | 4b9e2d8fce4a81d71c33c635716a0053e350e0ea /tactics | |
| parent | a5d336774c7b5342c8d873d43c9b92bae42b43e7 (diff) | |
CLEANUP: removing calls of the "Context.Named.Declaration.get_value" function
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |