diff options
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 895561324b..458714403a 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -503,8 +503,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not (* Compute interpretation metadatas *) let indimpls = List.map (fun impls -> userimpls @ impls) indimpls in - let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in - let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in + let impls = compute_internalization_env env_uparams sigma ~impls Inductive indnames fullarities indimpls in + let ntn_impls = compute_internalization_env env_uparams sigma Inductive indnames fullarities indimpls in let ninds = List.length indl in let (sigma, _), constructors = |