diff options
| author | Maxime Dénès | 2018-10-09 16:45:34 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-26 13:31:29 +0200 |
| commit | 8361be1d785f8588d2d3c2a0df7a1d9239bae5a1 (patch) | |
| tree | b44c6f8bed7e8f4ea09807b1239ab6ee3676aeeb /kernel/typeops.mli | |
| parent | e2096b9e6048bbab5c6da279bab3c3a719dc237f (diff) | |
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 57acdfe4b5..9312b993df 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. } *) |