From f93684a412f067622a5026c406bc76032c30b6e9 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 2 Apr 2019 22:39:32 +0200
Subject: Declare type of primitives in CPrimitives

Rather than in typeops
---
 library/global.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/global.mli b/library/global.mli
index f8b1f35f4d..0570ad0102 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -157,7 +157,7 @@ val is_type_in_type : GlobRef.t -> bool
 (** {6 Retroknowledge } *)
 
 val register_inline : Constant.t -> unit
-val register_inductive : inductive -> CPrimitives.prim_ind -> unit
+val register_inductive : inductive -> 'a CPrimitives.prim_ind -> unit
 
 (** {6 Oracle } *)
 
-- 
cgit v1.2.3