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.
---
 plugins/ltac/rewrite.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 914dc96648..67d09acfda 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1902,8 +1902,9 @@ let declare_projection name instance_id r =
   let types = Some (it_mkProd_or_LetIn typ ctx) in
   let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in
   let impargs, udecl = [], UState.default_univ_decl in
+  let info = Declare.CInfo.make ~scope ~kind ~opaque ~impargs ~udecl ~poly () in
   let _r : GlobRef.t =
-    Declare.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
+    Declare.declare_definition ~name ~info ~types ~body sigma
   in ()
 
 let build_morphism_signature env sigma m =
-- 
cgit v1.2.3