diff options
| author | Gaëtan Gilbert | 2020-03-10 14:19:30 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-10 14:19:30 +0100 |
| commit | cffb0ed6f58188b8ea01d54a5349d28313b86dc1 (patch) | |
| tree | 21c770ded4937e00419947f4ae31840217ce4978 /pretyping/evarsolve.ml | |
| parent | f1188b9a3f32eef7657bb46026447718f6fb6055 (diff) | |
| parent | 74df1a17d7d58d4fa99de58899e08de5bbe97810 (diff) | |
Merge PR #11764: Simplify mutual template polymorphism
Reviewed-by: SkySkimmer
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index aafd662f7d..c9ccd668ca 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -78,9 +78,9 @@ let get_polymorphic_positions env sigma f = match EConstr.kind sigma f with | Ind (ind, u) | Construct ((ind, _), u) -> let mib,oib = Inductive.lookup_mind_specif env ind in - (match oib.mind_arity with - | RegularArity _ -> assert false - | TemplateArity templ -> templ.template_param_levels) + (match mib.mind_template with + | None -> assert false + | Some templ -> templ.template_param_levels) | _ -> assert false let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) |