Possible code compaction motivated by Enrico's remark: https://github.com/math-comp/math-comp/pull/58#discussion_r76048943

1 files changed, 5 insertions, 9 deletions

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)