diff options
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 790e83dbe..101c14266 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -333,7 +333,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = List.iter check_param paramsl; let env0 = Global.env() in let pl = (List.hd indl).ind_univs in - let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in + let sigma, decl = interp_univ_decl_opt env0 pl in let sigma, (impls, ((env_params, ctx_params), userimpls)) = interp_context_evars env0 sigma paramsl in |