From 6bc53af07a100aad305393edb14c4a3d73b3e3b7 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 24 Aug 2016 16:01:35 +0200
Subject: Possible code compaction motivated by Enrico's remark: 
 https://github.com/math-comp/math-comp/pull/58#discussion_r76048943

---
 mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 14 +++++---------
 1 file changed, 5 insertions(+), 9 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index f7c2bf0..6fa7235 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -2090,15 +2090,11 @@ let abs_wgen keep_let ist f gen (gl,args,c) =
   match gen with
   | _, Some ((x, mode), None) when mode = "@" || (mode = " " && keep_let) ->
      let x = hoi_id x in
-     (match pf_get_hyp gl x with
-     | LocalAssum (_,ty) ->
-         gl,
-         mkVar x :: args,
-         mkProd_or_LetIn (RelDecl.LocalAssum (Name (f x),ty)) (subst_var x c)
-     | LocalDef (_,b,ty) ->
-         gl,
-         args,
-         mkProd_or_LetIn (RelDecl.LocalDef (Name (f x),b,ty)) (subst_var x c))
+     let decl = pf_get_hyp gl x in
+     gl,
+     (if NamedDecl.is_local_def decl then args else mkVar x :: args),
+     mkProd_or_LetIn (decl |> NamedDecl.to_rel |> RelDecl.set_name (Name (f x)))
+                     (subst_var x c)
   | _, Some ((x, _), None) ->
      let x = hoi_id x in
      gl, mkVar x :: args, mkProd (Name (f x),pf_get_hyp_typ gl x, subst_var x c)
-- 
cgit v1.2.3