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
---
 kernel/safe_typing.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/safe_typing.mli')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b2f6668577..ae6993b0e2 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -226,7 +226,7 @@ val mind_of_delta_kn_senv : safe_environment -> KerName.t -> MutInd.t
 (** {6 Retroknowledge / Native compiler } *)
 
 val register_inline : Constant.t -> safe_transformer0
-val register_inductive : inductive -> CPrimitives.prim_ind -> safe_transformer0
+val register_inductive : inductive -> 'a CPrimitives.prim_ind -> safe_transformer0
 
 val set_strategy :
   Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_transformer0
-- 
cgit v1.2.3