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 /pretyping | |
| parent | 27266c1f79e565a6a19da4c79fc1ce83f748e31c (diff) | |
| parent | ec80d04cfb4075922386dc8517577fd4819f1912 (diff) | |
Merge PR #8684: Remove a few circumvolutions around parameters of inductive entries
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/inferCumulativity.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index a56a8314e6..422a05c19a 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -196,7 +196,7 @@ let infer_inductive env mie = Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances) LMap.empty uarray in - let env, _ = Typeops.infer_local_decls env params in + let env = Typeops.check_context env params in let variances = List.fold_left (fun variances entry -> let variances = infer_arity_constructor true env variances entry.mind_entry_arity |