From 1f121ebf2990dc25899f2f3eb138eddd147483cf Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 15 May 2020 02:42:38 +0200
Subject: [declare] Refactor constant information into a record.

This improves the interface, and allows even more sealing of the API.

This is yet work in progress.
---
 vernac/comFixpoint.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'vernac/comFixpoint.ml')

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 5bf3350777..925a2d8389 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -283,9 +283,10 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   let fixdefs = List.map Option.get fixdefs in
   let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
   let fix_kind = Decls.IsDefinition fix_kind in
+  let info = Declare.CInfo.make ~scope ~opaque:false ~kind:fix_kind ~poly ~udecl () in
   let _ : GlobRef.t list =
-    Declare.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx
-      ~possible_indexes:indexes ~udecl ~ntns ~rec_declaration
+    Declare.declare_mutually_recursive ~info ~uctx
+      ~possible_indexes:indexes ~ntns ~rec_declaration
       fixitems
   in
   ()
-- 
cgit v1.2.3