From 456b282bef4ccdd5e67fdac4e938d02fce0f6901 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 29 Mar 2019 09:27:42 +0000
Subject: [Canonical structures] Minor refactoring

---
 vernac/record.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/record.ml b/vernac/record.ml
index 23274040b0..cb67548667 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -443,7 +443,7 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki
     let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
     let build = ConstructRef cstr in
     let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
-    let () = Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs) in
+    let () = Recordops.declare_structure(cstr, List.rev kinds, List.rev sp_projs) in
     rsp
   in
   List.mapi map record_data
-- 
cgit v1.2.3