diff options
| author | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
| commit | c70412ec8b0bb34b7a5607c07d34607a147d834c (patch) | |
| tree | 0cc6cd76a8f70dfd2f5b55b0db96db4de2ff07a2 /kernel/safe_typing.mli | |
| parent | 720ee2730684cc289cef588482323d177e0bea59 (diff) | |
| parent | 191e253d1d1ebd6c76c63b3d83f4228e46196a6e (diff) | |
Merge PR #6914: Primitive integers
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 57b01f15e3..1b7239da23 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -217,12 +217,8 @@ val mind_of_delta_kn_senv : safe_environment -> KerName.t -> MutInd.t (** {6 Retroknowledge / Native compiler } *) -open Retroknowledge - -val register : - field -> GlobRef.t -> safe_transformer0 - val register_inline : Constant.t -> safe_transformer0 +val register_inductive : inductive -> CPrimitives.prim_ind -> safe_transformer0 val set_strategy : Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_transformer0 |