diff options
| author | Pierre Roux | 2019-04-02 22:39:32 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:19:59 +0100 |
| commit | f93684a412f067622a5026c406bc76032c30b6e9 (patch) | |
| tree | 94965ae5e5d454b0ebb0d4266dd8a27f5487ddf3 /library | |
| parent | 6694a1811dc4e961a81fb4464cf5aaf05f1b5752 (diff) | |
Declare type of primitives in CPrimitives
Rather than in typeops
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 } *) |