diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-04-26 15:24:35 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:16 +0200 |
| commit | 7b5fcef8a0fb3b97a3980f10596137234061990f (patch) | |
| tree | 41512a4619f9b68641cb9da31b56059846e8a0b9 /library | |
| parent | 40f56eb0f79e208fc4b1b4ed2f0fb49c69c13a2f (diff) | |
Fix bugs
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) |