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/indtypes.ml | |
| parent | e2096b9e6048bbab5c6da279bab3c3a719dc237f (diff) | |
Remove a few circumvolutions around parameters of inductive entries
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b976469ff7..0346026aa4 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -271,7 +271,8 @@ let typecheck_inductive env mie = | Polymorphic_ind_entry ctx -> push_context ctx env | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env in - let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in + let env_params = check_context env' mie.mind_entry_params in + let paramsctxt = mie.mind_entry_params in (* We first type arity of each inductive definition *) (* This allows building the environment of arities and to share *) (* the set of constraints *) |