diff options
| author | Gaëtan Gilbert | 2018-08-23 10:54:19 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-13 14:03:04 +0200 |
| commit | e8937bfe903c7acbdfaa9d65bc0f5aaaa74a2bae (patch) | |
| tree | 75d9b7b0ec03713d2e2abd46ec24e745d8a2fae9 /vernac/comInductive.ml | |
| parent | c3b71e45db77f0875a8080275c6a1ae4b353d68d (diff) | |
Elaboration: do not ask small inductives to be template
This doesn't change behaviour currently as the kernel also makes this
decision, but in the future it won't.
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 18cd56aefc..0ca1bfd0c0 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -410,6 +410,7 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly let arities = List.map nf arities in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in + let arityconcl = List.map (Option.map (EConstr.ESorts.kind sigma)) arityconcl in let sigma = restrict_inductive_universes sigma ctx_params arities constructors in let uctx = Evd.check_univ_decl ~poly sigma decl in List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities; @@ -422,7 +423,7 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly let entries = List.map4 (fun ind arity concl (cnames,ctypes,cimpls) -> { mind_entry_typename = ind.ind_name; mind_entry_arity = arity; - mind_entry_template = Option.has_some concl; + mind_entry_template = Option.cata (fun s -> not (Sorts.is_small s)) false concl; mind_entry_consnames = cnames; mind_entry_lc = ctypes }) indl arities arityconcl constructors in |