From 9c4f68936e33c93cf179eec6e996062bec918915 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 26 Aug 2016 16:34:53 +0200
Subject: fix compilation wrt. commit 69388fc in Coq trunk

---
 mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/ssreflect/plugin')

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index 6fa7235..ee13c15 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -2093,7 +2093,7 @@ let abs_wgen keep_let ist f gen (gl,args,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)))
+     mkProd_or_LetIn (decl |> NamedDecl.to_rel_decl |> RelDecl.set_name (Name (f x)))
                      (subst_var x c)
   | _, Some ((x, _), None) ->
      let x = hoi_id x in
-- 
cgit v1.2.3