diff options
| author | Gaëtan Gilbert | 2018-10-26 18:25:34 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-26 18:25:34 +0200 |
| commit | be144dcaa1d1d8ff22e9e39f49fd247e813ac1f8 (patch) | |
| tree | 075437b5eefd1b526acdf13d00b25fdec3765213 /kernel/typeops.mli | |
| parent | 27266c1f79e565a6a19da4c79fc1ce83f748e31c (diff) | |
| parent | ec80d04cfb4075922386dc8517577fd4819f1912 (diff) | |
Merge PR #8684: Remove a few circumvolutions around parameters of inductive entries
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 1fd070d9d5..d24002065b 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -12,7 +12,6 @@ open Names open Constr open Univ open Environ -open Entries (** {6 Typing functions (not yet tagged as safe) } @@ -27,8 +26,8 @@ val infer : env -> constr -> unsafe_judgment val infer_v : env -> constr array -> unsafe_judgment array val infer_type : env -> types -> unsafe_type_judgment -val infer_local_decls : - env -> (Id.t * local_entry) list -> (env * Constr.rel_context) +val check_context : + env -> Constr.rel_context -> env (** {6 Basic operations of the typing machine. } *) |