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 /kernel/safe_typing.ml | |
| parent | 6694a1811dc4e961a81fb4464cf5aaf05f1b5752 (diff) | |
Declare type of primitives in CPrimitives
Rather than in typeops
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e846b17aa0..52bd9a6ada 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1327,7 +1327,7 @@ let register_inline kn senv = let cb = {cb with const_inline_code = true} in let env = add_constant kn cb env in { senv with env} -let check_register_ind ind r env = +let check_register_ind (type t) ind (r : t CPrimitives.prim_ind) env = let (mb,ob as spec) = Inductive.lookup_mind_specif env ind in let check_if b msg = if not b then |