diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/library/declare.ml b/library/declare.ml index fcaadaa6e..bf5313545 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -364,9 +364,9 @@ let infer_inductive_subtyping (pth, mind_ent) = let env' = Environ.push_context (Univ.UInfoInd.univ_context mind_ent.mind_entry_universes) env in - let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in - let evd = Evd.from_env env'' in - (pth, Inductiveops.infer_inductive_subtyping env'' evd mind_ent) + (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *) + let evd = Evd.from_env env' in + (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent) end else (pth, mind_ent) |