diff options
| author | Gaëtan Gilbert | 2020-02-20 16:31:53 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-31 14:39:43 +0200 |
| commit | f19cf4259f63a9c0392c922527e0e9002192949e (patch) | |
| tree | 5f0cf9440e877bf8f1e6b94c13776b8e4060da1d /vernac/comInductive.ml | |
| parent | c0a71f9ff6289d99bbbcd13ef65c68f74ac9e191 (diff) | |
Remove check_hidden_implicit_parameters (not needed anymore)
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 = |